let M be non empty set ; :: thesis: for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds
M |= F1 \/ F2
let F1, F2 be Subset of WFF; :: thesis: ( M |= F1 & M |= F2 implies M |= F1 \/ F2 )
assume A1: ( M |= F1 & M |= F2 ) ; :: thesis: M |= F1 \/ F2
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in F1 \/ F2 implies M |= H )
assume H in F1 \/ F2 ; :: thesis: M |= H
then ( H in F1 or H in F2 ) by XBOOLE_0:def 3;
hence M |= H by A1; :: thesis: verum