| ⊢ | f ⊃ g ⇒ ⊢ f+ ⊃ g+ | ChopPlusImpChopPlus |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ f+ ≡ f ∨ (f ∧more) ; f+ | |
3 | ⊢ g+ ≡ g ∨ (g ∧more) ; g+ | |
4 | ⊢ f+ ∧¬(g+) ⊃ ((f ∧more) ; f+) ∧¬((g ∧more) ; g+) | |
5 | ⊢ f ∧more ⊃ g ∧more | |
6 | ⊢ (f ∧more) ; f+ ⊃ (g ∧more) ; f+ | |
7 | ⊢ f+ ∧¬(g+) ⊃ ((g ∧more) ; f+) ∧¬((g ∧more) ; g+) | |
8 | ⊢ g ∧more ⊃more | |
9 | ⊢ f+ ⊃ g+ |
qed