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: 'not' H is negative ;
then H = the_argument_of ('not' H) by ZF_LANG:def 30;
then A2: St (('not' H),E) = (VAL E) \ (St (H,E)) by 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 A2, 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 A2, XBOOLE_0:def 5; :: thesis: verum