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
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 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;
hence Y is Field_Subset of X by A1; :: thesis: verum