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

proof

given x1, x2 being Variable such that A1: H = x1 '=' x2 ; :: according to ZF_LANG:def 10 :: thesis: H / x,y is being_equality
ex z1, z2 being Variable st H / x,y = z1 '=' z2 by A1, Th167;
hence H / x,y is being_equality by ZF_LANG:16; :: thesis: verum

end;

assume H / x,y is being_equality ; :: thesis: H is being_equality
then A2: (H / x,y) . 1 = 0 by ZF_LANG:35;
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 <> 0 by Th148;
then H . 1 <> x by A2, A3, Def4;
then 0 = H . 1 by A2, A3, Def4;
hence H is being_equality by ZF_LANG:41; :: thesis: verum