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

proof

given H1, H2 being ZF-formula such that A1: H = H1 '&' H2 ; :: according to ZF_LANG:def 13 :: thesis: H / x,y is conjunctive
H / x,y = (H1 / x,y) '&' (H2 / x,y) by A1, Th172;
hence H / x,y is conjunctive by ZF_LANG:16; :: thesis: verum

end;

assume A2: H / x,y is conjunctive ; :: thesis: H is conjunctive
( 1 <= 3 & 3 <= len H ) by ZF_LANG:29;
then ( 1 <= 1 & 1 <= len H ) by XXREAL_0:2;
then A3: ( (H / x,y) . 1 = 3 & y <> 3 & 1 in dom H ) by A2, Th148, FINSEQ_3:27, ZF_LANG:38;
then H . 1 <> x by Def4;
then 3 = H . 1 by A3, Def4;
hence H is conjunctive by ZF_LANG:44; :: thesis: verum