let H be ZF-formula; :: thesis: for E being non empty set st H is being_membership holds
for f being Function of VAR,E holds
( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) )
let E be non empty set ; :: thesis: ( H is being_membership implies for f being Function of VAR,E holds
( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) )
assume H is being_membership ; :: thesis: for f being Function of VAR,E holds
( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) )
then H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
hence for f being Function of VAR,E holds
( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) by Th3; :: thesis: verum