theorem Th19: :: ZF_LANG:19

for H being ZF-formula st H is being_membership holds
H . 1 = 1