let H be ZF-formula; :: thesis: ( H is being_membership implies H . 1 = 1 )
assume H is being_membership ; :: thesis: H . 1 = 1
then consider x, y being Variable such that
A1: H = x 'in' y ;
H = <*1,x,y*> by A1, FINSEQ_1:def 10;
hence H . 1 = 1 by FINSEQ_1:45; :: thesis: verum