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:31;
A2: 'not' H is negative by ZF_LANG:16;
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 Def2;
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