let p, q, r be ZF-formula; :: thesis: 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) )
let M be non empty set ; :: thesis: 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) )
let v be Function of VAR,M; :: thesis: ( M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) & M |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) )

now :: thesis: for v being Function of VAR,M holds M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r)

let v be Function of VAR,M; :: thesis: M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r)

now :: thesis: ( M,v |= (p => r) '&' (q => r) implies M,v |= (p 'or' q) => r )

assume M,v |= (p => r) '&' (q => r) ; :: thesis: M,v |= (p 'or' q) => r
then ( M,v |= p => r & M,v |= q => r ) by ZF_MODEL:15;
then ( ( M,v |= p or M,v |= q ) implies M,v |= r ) by ZF_MODEL:18;
then ( M,v |= p 'or' q implies M,v |= r ) by ZF_MODEL:17;
hence M,v |= (p 'or' q) => r by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) by ZF_MODEL:18; :: thesis: verum

end;

hence ( M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) & M |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) ) ; :: thesis: verum