theorem :: ZF_LANG1:117

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