theorem :: ZF_LANG1:120

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