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

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