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 by ZF_LANG:16;
then ( H = the_argument_of ('not' H) & union {(St H,E)} = St H,E ) by ZFMISC_1:31, ZF_LANG:def 30;
then A2: St ('not' H),E = (VAL E) \ (St H,E) by A1, Lm3;
thus ( not f in St H,E implies f in St ('not' H),E ) :: thesis: ( f in St ('not' H),E implies not f in St H,E )

proof

f in VAL E by Def2;
hence ( not f in St H,E implies f in St ('not' H),E ) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

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