theorem Th37: :: ZF_LANG:37

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