let H be ZF-formula; :: thesis: ( H is being_membership implies H = (Var1 H) 'in' (Var2 H) )
assume A1: H is being_membership ; :: thesis: H = (Var1 H) 'in' (Var2 H)
then consider x, y being Variable such that
A2: H = x 'in' y by Def11;
A3: ( H = (<*1*> ^ <*x*>) ^ <*y*> & (<*1*> ^ <*x*>) ^ <*y*> = <*1,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) 'in' (Var2 H) by A2; :: thesis: verum