| ⊢ | (f ∨ f1) ; g ≡ f ; g ∨ f1 ; g | OrChopEqv |
The proof for ⊂ is immediate from axiom OrChopImp.
Here is the proof for the converse:
1 | ⊢ f ⊃ f ∨ f1 | |
2 | ⊢ f ; g ⊃ (f ∨ f1) ; g | |
3 | ⊢ f1 ⊃ f ∨ f1 | |
4 | ⊢ f1 ; g ⊃ (f ∨ f1) ; g | |
5 | ⊢ f ; g ∨ f ; g1 ⊃ (f ∨ f1) ; g |
qed