theorem :: ZF_LANG1:123

for p, q being ZF-formula
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)) )