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 )
A1: ( E,f |= 'not' H iff f in St (('not' H),E) ) by Def4;
( E,f |= H iff f in St (H,E) ) by Def4;
hence ( E,f |= H iff not E,f |= 'not' H ) by A1, Th4; :: thesis: verum