let H be ZF-formula; :: thesis: ( H is negative implies H . 1 = 2 )
assume H is negative ; :: thesis: H . 1 = 2
then consider H1 being ZF-formula such that
A1: H = 'not' H1 by Def12;
thus H . 1 = 2 by A1, FINSEQ_1:58; :: thesis: verum