let X, Y be set ; :: thesis: ( Y is SigmaField of X implies Y is Field_Subset of X )

assume A1: Y is SigmaField of X ; :: thesis: Y is Field_Subset of X

Y is cap-closed

assume A1: Y is SigmaField of X ; :: thesis: Y is Field_Subset of X

Y is cap-closed

proof

hence
Y is Field_Subset of X
by A1; :: thesis: verum
let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in Y or not B in Y or A /\ B in Y )

assume A2: ( A in Y & B in Y ) ; :: thesis: A /\ B in Y

then reconsider A9 = A, B9 = B as Subset of X by A1;

set A1 = A9 followed_by B9;

rng (A9 followed_by B9) = {A9,B9} by FUNCT_7:126;

then A3: rng (A9 followed_by B9) c= Y by A2, ZFMISC_1:32;

Intersection (A9 followed_by B9) = A /\ B by Th14;

hence A /\ B in Y by A1, A3, Def6; :: thesis: verum

end;assume A2: ( A in Y & B in Y ) ; :: thesis: A /\ B in Y

then reconsider A9 = A, B9 = B as Subset of X by A1;

set A1 = A9 followed_by B9;

rng (A9 followed_by B9) = {A9,B9} by FUNCT_7:126;

then A3: rng (A9 followed_by B9) c= Y by A2, ZFMISC_1:32;

Intersection (A9 followed_by B9) = A /\ B by Th14;

hence A /\ B in Y by A1, A3, Def6; :: thesis: verum