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