let Y, X 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

proof

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 A' = A, B' = B as Subset of by A1;
set A1 = A' followed_by B';
rng (A' followed_by B') = {A',B'} by FUNCT_7:128;
then A3: rng (A' followed_by B') c= Y by A2, ZFMISC_1:38;
Intersection (A' followed_by B') = A /\ B by Th30;
hence A /\ B in Y by A1, A3, Def8; :: thesis: verum

end;

hence Y is Field_Subset of X by A1; :: thesis: verum