theorem :: ZF_LANG1:118

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