let p, q be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )
let M be non empty set ; :: thesis: for v being Function of VAR,M holds
( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )
let v be Function of VAR,M; :: thesis: ( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )

now :: thesis: for v being Function of VAR,M holds M,v |= (p => ('not' q)) => (q => ('not' p))

let v be Function of VAR,M; :: thesis: M,v |= (p => ('not' q)) => (q => ('not' p))

now :: thesis: ( M,v |= p => ('not' q) implies M,v |= q => ('not' p) )

assume M,v |= p => ('not' q) ; :: thesis: M,v |= q => ('not' p)
then ( M,v |= p implies M,v |= 'not' q ) by ZF_MODEL:18;
then ( M,v |= q implies M,v |= 'not' p ) by ZF_MODEL:14;
hence M,v |= q => ('not' p) by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (p => ('not' q)) => (q => ('not' p)) by ZF_MODEL:18; :: thesis: verum

end;

hence ( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) ) ; :: thesis: verum