theorem :: ZF_LANG:24

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