theorem :: ZF_LANG:26

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