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 ) by Th153; :: thesis: ( H / (x,y) is being_equality implies H is being_equality )
assume H / (x,y) is being_equality ; :: thesis: H is being_equality
then A1: (H / (x,y)) . 1 = 0 by ZF_LANG:18;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then A2: 1 in dom H by FINSEQ_3:25;
y <> 0 by Th135;
then H . 1 <> x by A1, A2, Def3;
then 0 = H . 1 by A1, A2, Def3;
hence H is being_equality by ZF_LANG:24; :: thesis: verum