theorem :: ZF_LANG1:124

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' q)) => (('not' p) '&' ('not' q)) & M |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) )