let X be set ; :: thesis: for F being Field_Subset of X holds
( F is SigmaField of X iff F is MonotoneClass of X )
let F be Field_Subset of X; :: thesis: ( F is SigmaField of X iff F is MonotoneClass of X )
thus ( F is SigmaField of X implies F is MonotoneClass of X ) :: thesis: ( F is MonotoneClass of X implies F is SigmaField of X )

proof

assume F is SigmaField of X ; :: thesis: F is MonotoneClass of X
then reconsider F = F as SigmaField of X ;
A1: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= F holds
Union A1 in F

proof

let A1 be SetSequence of X; :: thesis: ( A1 is non-descending & rng A1 c= F implies Union A1 in F )
assume that
A1 is non-descending and
A2: rng A1 c= F ; :: thesis: Union A1 in F
reconsider A2 = A1 as SetSequence of F by A2, RELAT_1:def 19;
Union A2 in F by PROB_1:17;
hence Union A1 in F ; :: thesis: verum

end;

F is non-increasing-closed by PROB_1:def 6;
hence F is MonotoneClass of X by A1, Def7; :: thesis: verum

end;

assume A3: F is MonotoneClass of X ; :: thesis: F is SigmaField of X
for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F

proof

let A1 be SetSequence of X; :: thesis: ( rng A1 c= F implies Intersection A1 in F )
assume A4: rng A1 c= F ; :: thesis: Intersection A1 in F
set A2 = Partial_Intersection A1;
defpred S₁[ Nat] means (Partial_Intersection A1) . $1 in F;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: (Partial_Intersection A1) . k in F ; :: thesis: S₁[k + 1]
( A1 . (k + 1) in rng A1 & (Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) ) by Def1, NAT_1:51;
hence (Partial_Intersection A1) . (k + 1) in F by A4, A6, FINSUB_1:def 2; :: thesis: verum

end;

( A1 . 0 in rng A1 & (Partial_Intersection A1) . 0 = A1 . 0 ) by Def1, NAT_1:51;
then A7: S₁[ 0 ] by A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A5);
then A8: rng (Partial_Intersection A1) c= F by NAT_1:52;
Partial_Intersection A1 is non-ascending by Th10;
then Intersection (Partial_Intersection A1) in F by A3, A8, Def8;
hence Intersection A1 in F by Th14; :: thesis: verum

end;

hence F is SigmaField of X by PROB_1:def 6; :: thesis: verum