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 )
set G = H / (x,y);
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, Th161;
hence H / (x,y) is disjunctive ; :: thesis: verum
end;
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;
then H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9 ;
A4: ('not' G1) '&' ('not' G2) = H9 / (x,y) by A2, A3, Th156;
then H9 / (x,y) is conjunctive ;
then H9 is conjunctive by Th169;
then consider H1, H2 being ZF-formula such that
A5: H9 = H1 '&' H2 ;
'not' G2 = H2 / (x,y) by A4, A5, Th158;
then H2 / (x,y) is negative ;
then H2 is negative by Th168;
then consider p2 being ZF-formula such that
A6: H2 = 'not' p2 ;
'not' G1 = H1 / (x,y) by A4, A5, Th158;
then H1 / (x,y) is negative ;
then H1 is negative by Th168;
then consider p1 being ZF-formula such that
A7: H1 = 'not' p1 ;
H = p1 'or' p2 by A3, A5, A7, A6;
hence H is disjunctive ; :: thesis: verum