let G1, G2, H1, H2 be ZF-formula; :: thesis: for x, y being Variable holds
( G1 'or' G2 = (H1 'or' H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) )
let x, y be Variable; :: thesis: ( G1 'or' G2 = (H1 'or' H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) )
( ( 'not' G1 = ('not' H1) / x,y & 'not' G2 = ('not' H2) / x,y ) iff ('not' G1) '&' ('not' G2) = (('not' H1) '&' ('not' H2)) / x,y ) by Th172;
hence ( G1 'or' G2 = (H1 'or' H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) ) by Th170; :: thesis: verum