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

now

let v be Function of VAR ,M; :: thesis: M,v |= q => (p 'or' q)
( M,v |= q implies M,v |= p 'or' q ) by ZF_MODEL:17;
hence M,v |= q => (p 'or' q) by ZF_MODEL:18; :: thesis: verum

end;

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