let X be set ; :: thesis: for F being Field_Subset of X
for A, B being set st A in F & B in F holds
A \/ B in F
let F be Field_Subset of X; :: thesis: for A, B being set st A in F & B in F holds
A \/ B in F
let A, B be set ; :: thesis: ( A in F & B in F implies A \/ B in F )
assume A1: ( A in F & B in F ) ; :: thesis: A \/ B in F
then reconsider A1 = A, B1 = B as Subset of X ;
( A1 ` in F & B1 ` in F ) by A1, Def1;
then (A1 `) /\ (B1 `) in F by FINSUB_1:def 2;
then (A1 \/ B1) ` in F by XBOOLE_1:53;
then ((A1 \/ B1) `) ` in F by Def1;
hence A \/ B in F ; :: thesis: verum