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 )

for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F

( 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 A3:
F is MonotoneClass of X
; :: thesis: F is SigmaField of X
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 V75() & rng A1 c= F holds

Union A1 in F

hence F is MonotoneClass of X by A1, Def7; :: thesis: verum

end;then reconsider F = F as SigmaField of X ;

A1: for A1 being SetSequence of X st A1 is V75() & rng A1 c= F holds

Union A1 in F

proof

F is non-increasing-closed
by PROB_1:def 6;
let A1 be SetSequence of X; :: thesis: ( A1 is V75() & rng A1 c= F implies Union A1 in F )

assume that

A1 is V75() 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;assume that

A1 is V75() 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

hence F is MonotoneClass of X by A1, Def7; :: thesis: verum

for A1 being SetSequence of X st rng A1 c= F holds

Intersection A1 in F

proof

hence
F is SigmaField of X
by PROB_1:def 6; :: thesis: verum
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_{1}[ Nat] means (Partial_Intersection A1) . $1 in F;

A5: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A7: S_{1}[ 0 ]
by A4;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A7, A5);

then A8: rng (Partial_Intersection A1) c= F by NAT_1:52;

Partial_Intersection A1 is V74() by Th10;

then Intersection (Partial_Intersection A1) in F by A3, A8, Def8;

hence Intersection A1 in F by Th14; :: thesis: verum

end;assume A4: rng A1 c= F ; :: thesis: Intersection A1 in F

set A2 = Partial_Intersection A1;

defpred S

A5: for k being Nat st S

S

proof

( A1 . 0 in rng A1 & (Partial_Intersection A1) . 0 = A1 . 0 )
by Def1, NAT_1:51;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: (Partial_Intersection A1) . k in F ; :: thesis: S_{1}[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;assume A6: (Partial_Intersection A1) . k in F ; :: thesis: S

( 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

then A7: S

for k being Nat holds S

then A8: rng (Partial_Intersection A1) c= F by NAT_1:52;

Partial_Intersection A1 is V74() by Th10;

then Intersection (Partial_Intersection A1) in F by A3, A8, Def8;

hence Intersection A1 in F by Th14; :: thesis: verum