let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )
let M be non empty set ; :: thesis: for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )
let v be Function of VAR,M; :: thesis: ( H is negative implies ( M,v |= H iff not M,v |= the_argument_of H ) )
assume H is negative ; :: thesis: ( M,v |= H iff not M,v |= the_argument_of H )
then H = 'not' (the_argument_of H) by ZF_LANG:def 30;
hence ( M,v |= H iff not M,v |= the_argument_of H ) by ZF_MODEL:14; :: thesis: verum