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