for H being ZF-formula st H is being_membership holds
H = (Var1 H) 'in' (Var2 H)