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 ;
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 A1: ( A1 is non-descending & rng A1 c= F ) ; :: thesis: Union A1 in F
reconsider A2 = A1 as SetSequence of by RELAT_1:def 19, A1;
Union A2 in F by PROB_1:46;
hence Union A1 in F ; :: thesis: verum

end;

then A2: F is non-decreasing-closed by Def12;
F is non-increasing-closed

proof

let A1 be SetSequence of X; :: according to PROB_3:def 13 :: thesis: ( A1 is non-ascending & rng A1 c= F implies Intersection A1 in F )
assume A1 is non-ascending ; :: thesis: ( not rng A1 c= F or Intersection A1 in F )
assume rng A1 c= F ; :: thesis: Intersection A1 in F
hence Intersection A1 in F by PROB_1:def 8; :: thesis: verum

end;

hence F is MonotoneClass of X by A2; :: thesis: verum

end;

assume F is MonotoneClass of X ; :: thesis: F is SigmaField of X
then A3: ( F is non-increasing-closed & F is non-decreasing-closed ) ;
( ( for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F ) & ( for A being Subset of X st A in F holds
A ` in F ) )

proof

thus for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F :: thesis: for A being Subset of X st A in F holds
A ` 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;
X: A1 . 0 in rng A1 by NAT_1:52;
(Partial_Intersection A1) . 0 = A1 . 0 by Def1;
then A5: S₁[ 0 ] by A4, X;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then X: rng (Partial_Intersection A1) c= F by NAT_1:53;
Partial_Intersection A1 is non-ascending by Th12;
then Intersection (Partial_Intersection A1) in F by A3, Def13, X;
hence Intersection A1 in F by Th16; :: thesis: verum

end;

thus for A being Subset of X st A in F holds
A ` in F by PROB_1:def 1; :: thesis: verum

end;

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