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

proof

given H1 being ZF-formula such that A1: H = 'not' H1 ; :: according to ZF_LANG:def 12 :: thesis: H / x,y is negative
H / x,y = 'not' (H1 / x,y) by A1, Th170;
hence H / x,y is negative by ZF_LANG:16; :: thesis: verum

end;

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