let X be set ; :: thesis: for S being non empty Subset-Family of X holds
( S is Field_Subset of X iff for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) )
let S be non empty Subset-Family of X; :: thesis: ( S is Field_Subset of X iff for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) )

hereby :: thesis: ( ( for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) ) implies S is Field_Subset of X )

assume A1: S is Field_Subset of X ; :: thesis: for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) )
for A, B being set st A in S & B in S holds
A /\ B in S

proof

let A, B be set ; :: thesis: ( A in S & B in S implies A /\ B in S )
assume A2: ( A in S & B in S ) ; :: thesis: A /\ B in S
then ( X \ A in S & X \ B in S ) by A1, Def3;
then A3: (X \ A) \/ (X \ B) in S by A1, FINSUB_1:def 1;
A /\ B c= A by XBOOLE_1:17;
then A /\ B = X /\ (A /\ B) by A2, XBOOLE_1:1, XBOOLE_1:28
.= X \ (X \ (A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;
hence A /\ B in S by A1, A3, Def3; :: thesis: verum

end;

hence for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) by A1, Def3; :: thesis: verum

end;

assume A4: for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) ; :: thesis: S is Field_Subset of X
then A5: for A being set st A in S holds
X \ A in S ;
for A, B being set st A in S & B in S holds
A \/ B in S

proof

let A, B be set ; :: thesis: ( A in S & B in S implies A \/ B in S )
assume A6: ( A in S & B in S ) ; :: thesis: A \/ B in S
then ( X \ A in S & X \ B in S ) by A4;
then A7: (X \ A) /\ (X \ B) in S by A4;
A \/ B = X /\ (A \/ B) by A6, XBOOLE_1:8, XBOOLE_1:28
.= X \ (X \ (A \/ B)) by XBOOLE_1:48
.= X \ ((X \ A) /\ (X \ B)) by XBOOLE_1:53 ;
hence A \/ B in S by A4, A7; :: thesis: verum

end;

then ( S is cup-closed & S is compl-closed ) by A5, Def3, FINSUB_1:def 1;
hence S is Field_Subset of X ; :: thesis: verum