let E be non empty set ; :: thesis: for f being Function of VAR ,E
for H being ZF-formula holds
( E,f |= H iff not E,f |= 'not' H )
let f be Function of VAR ,E; :: thesis: for H being ZF-formula holds
( E,f |= H iff not E,f |= 'not' H )
let H be ZF-formula; :: thesis: ( E,f |= H iff not E,f |= 'not' H )
( ( E,f |= H implies f in St H,E ) & ( f in St H,E implies E,f |= H ) & ( E,f |= 'not' H implies f in St ('not' H),E ) & ( f in St ('not' H),E implies E,f |= 'not' H ) & ( f in St H,E implies not f in St ('not' H),E ) & ( not f in St ('not' H),E implies f in St H,E ) ) by Def4, Th4;
hence ( E,f |= H iff not E,f |= 'not' H ) ; :: thesis: verum