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

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