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 that
A1: A in F and
A2: B in F ; :: thesis: A \/ B in F
reconsider A1 = A, B1 = B as Subset of X by A1, A2;
A3: A1 ` in F by A1, Def1;
B1 ` in F by A2, Def1;
then (A1 ` ) /\ (B1 ` ) in F by A3, 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