let H be ZF-formula; :: thesis: for x, y being Variable holds
( H is disjunctive iff H / x,y is disjunctive )
let x, y be Variable; :: thesis: ( H is disjunctive iff H / x,y is disjunctive )
thus ( H is disjunctive implies H / x,y is disjunctive ) :: thesis: ( H / x,y is disjunctive implies H is disjunctive )

proof

given H1, H2 being ZF-formula such that A1: H = H1 'or' H2 ; :: according to ZF_LANG:def 20 :: thesis: H / x,y is disjunctive
H / x,y = (H1 / x,y) 'or' (H2 / x,y) by A1, Th175;
hence H / x,y is disjunctive by ZF_LANG:22; :: thesis: verum

end;

set G = H / x,y;
given G1, G2 being ZF-formula such that A2: H / x,y = G1 'or' G2 ; :: according to ZF_LANG:def 20 :: thesis: H is disjunctive
H / x,y is negative by A2, ZF_LANG:16;
then H is negative by Th182;
then consider H' being ZF-formula such that
A3: H = 'not' H' by ZF_LANG:16;
A4: ('not' G1) '&' ('not' G2) = H' / x,y by A2, A3, Th170;
then H' / x,y is conjunctive by ZF_LANG:16;
then H' is conjunctive by Th183;
then consider H1, H2 being ZF-formula such that
A5: H' = H1 '&' H2 by ZF_LANG:16;
A6: ( 'not' G1 = H1 / x,y & 'not' G2 = H2 / x,y ) by A4, A5, Th172;
then H1 / x,y is negative by ZF_LANG:16;
then H1 is negative by Th182;
then consider p1 being ZF-formula such that
A7: H1 = 'not' p1 by ZF_LANG:16;
H2 / x,y is negative by A6, ZF_LANG:16;
then H2 is negative by Th182;
then consider p2 being ZF-formula such that
A8: H2 = 'not' p2 by ZF_LANG:16;
H = p1 'or' p2 by A3, A5, A7, A8;
hence H is disjunctive by ZF_LANG:22; :: thesis: verum