let X, M be set ; :: thesis:

hereby :: thesis:

assume A1: M is Field_Subset of X ; :: thesis:
then reconsider S = M as non empty Subset-Family of X ;
take S = S; :: thesis:
thus M = S ; :: thesis:
thus 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, FINSUB_1:def 1; :: thesis:

end;

given S being non empty Subset-Family of X such that A2: ( M = S & ( 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:
A3: S is cup-closed

proof

let A, B be set ; :: according to FINSUB_1:def 1 :: thesis:
assume ( A in S & B in S ) ; :: thesis:
hence A \/ B in S by A2; :: thesis:

end;

S is compl-closed

proof

let A be set ; :: according to MEASURE1:def 3 :: thesis:
assume A in S ; :: thesis:
hence X \ A in S by A2; :: thesis:

end;

hence M is Field_Subset of X by A2, A3; :: thesis: