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

now

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

now

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

end;

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

end;

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