let E be non empty set ; :: thesis: for H being ZF-formula
for f being Function of VAR,E holds
( not f in St (H,E) iff f in St (('not' H),E) )
let H be ZF-formula; :: thesis: for f being Function of VAR,E holds
( not f in St (H,E) iff f in St (('not' H),E) )
let f be Function of VAR,E; :: thesis: ( not f in St (H,E) iff f in St (('not' H),E) )
A1: union {(St (H,E))} = St (H,E) by ZFMISC_1:25;
A2: 'not' H is negative by ZF_LANG:5;
then H = the_argument_of ('not' H) by ZF_LANG:def 30;
then A3: St (('not' H),E) = (VAL E) \ (St (H,E)) by A2, A1, Lm3;
f in VAL E by FUNCT_2:8;
hence ( not f in St (H,E) implies f in St (('not' H),E) ) by A3, XBOOLE_0:def 5; :: thesis: ( f in St (('not' H),E) implies not f in St (H,E) )
assume f in St (('not' H),E) ; :: thesis: not f in St (H,E)
hence not f in St (H,E) by A3, XBOOLE_0:def 5; :: thesis: verum