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 by Def10;
A3: ( H = (<*0 *> ^ <*x*>) ^ <*y*> & (<*0 *> ^ <*x*>) ^ <*y*> = <*0 ,x,y*> ) by A2, FINSEQ_1:def 10;
H is atomic by A1, Def15;
then ( H . 2 = x & H . 3 = y & H . 2 = Var1 H & H . 3 = Var2 H ) by A3, Def28, Def29, FINSEQ_1:62;
hence H = (Var1 H) '=' (Var2 H) by A2; :: thesis: verum