theorem Th20: :: ZF_LANG:20

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