theorem :: ZF_LANG:25

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