let H be ZF-formula; :: thesis: ( H is being_equality implies H = (Var1 H) '=' (Var2 H) )
assume A1: H is being_equality ; :: thesis: H = (Var1 H) '=' (Var2 H)
then consider x, y being Variable such that
A2: H = x '=' y ;
(<*0*> ^ <*x*>) ^ <*y*> = <*0,x,y*> by FINSEQ_1:def 10;
then A3: ( H . 2 = x & H . 3 = y ) by A2;
A4: H is atomic by A1;
then H . 2 = Var1 H by Def28;
hence H = (Var1 H) '=' (Var2 H) by A2, A4, A3, Def29; :: thesis: verum