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

now

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

now

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

end;

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

end;

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