let H be ZF-formula; for x, y being Variable holds
( H is being_equality iff H / (x,y) is being_equality )
let x, y be Variable; ( 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; ( H / (x,y) is being_equality implies H is being_equality )
assume
H / (x,y) is being_equality
; 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; verum