:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

Lm1:  for t, p, s being real number st 0 < s &amp; t <= p holds
( t < p + s &amp; t - s < p )
proofend;

theorem Th1: :: PROB_3:1
for f being FinSequence holds not 0 in dom f
proofend;

theorem Th2: :: PROB_3:2
for n being Nat
for f being FinSequence holds
( n in dom f iff ( n <> 0 &amp; n <= len f ) )
proofend;

theorem Th3: :: PROB_3:3
for g being real number
for f being Real_Sequence st ex k being Nat st
for n being Nat st k <= n holds
f . n = g holds
( f is convergent &amp; lim f = g )
proofend;

theorem Th4: :: PROB_3:4
for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * ASeq) . n >= 0
proofend;

theorem Th5: :: PROB_3:5
for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq . n c= BSeq . n holds
(P * ASeq) . n <= (P * BSeq) . n
proofend;

theorem Th6: :: PROB_3:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V71() holds
P * ASeq is non-decreasing
proofend;

theorem Th7: :: PROB_3:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V70() holds
P * ASeq is non-increasing
proofend;

definition
let X be set ;
let A1 be SetSequence of X;
func Partial_Intersection A1 ->  SetSequence of X means :Def1: :: PROB_3:def 1
( it . 0 = A1 . 0 &amp; ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) );
existence
 ex b1 being SetSequence of X st
( b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) &amp; b2 . 0 = A1 . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) /\ (A1 . (n + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def_1_:_
 for X being set
for A1, b3 being SetSequence of X holds
( b3 = Partial_Intersection A1 iff ( b3 . 0 = A1 . 0 &amp; ( for n being Nat holds b3 . (n + 1) = (b3 . n) /\ (A1 . (n + 1)) ) ) );

definition
let X be set ;
let A1 be SetSequence of X;
func Partial_Union A1 ->  SetSequence of X means :Def2: :: PROB_3:def 2
( it . 0 = A1 . 0 &amp; ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) );
existence
 ex b1 being SetSequence of X st
( b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) &amp; b2 . 0 = A1 . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ (A1 . (n + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Partial_Union PROB_3:def_2_:_
 for X being set
for A1, b3 being SetSequence of X holds
( b3 = Partial_Union A1 iff ( b3 . 0 = A1 . 0 &amp; ( for n being Nat holds b3 . (n + 1) = (b3 . n) \/ (A1 . (n + 1)) ) ) );

theorem Th8: :: PROB_3:8
for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n
proofend;

theorem Th9: :: PROB_3:9
for n being Nat
for X being set
for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n
proofend;

theorem Th10: :: PROB_3:10
for X being set
for A1 being SetSequence of X holds Partial_Intersection A1 is V70()
proofend;

theorem Th11: :: PROB_3:11
for X being set
for A1 being SetSequence of X holds Partial_Union A1 is V71()
proofend;

theorem Th12: :: PROB_3:12
for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
proofend;

theorem Th13: :: PROB_3:13
for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n &amp; x in A1 . k ) )
proofend;

theorem Th14: :: PROB_3:14
for X being set
for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1
proofend;

theorem Th15: :: PROB_3:15
for X being set
for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1
proofend;

definition
let X be set ;
let A1 be SetSequence of X;
func Partial_Diff_Union A1 ->  SetSequence of X means :Def3: :: PROB_3:def 3
( it . 0 = A1 . 0 &amp; ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) );
existence
 ex b1 being SetSequence of X st
( b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )
proofend;
uniqueness
 for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) &amp; b2 . 0 = A1 . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def_3_:_
 for X being set
for A1, b3 being SetSequence of X holds
( b3 = Partial_Diff_Union A1 iff ( b3 . 0 = A1 . 0 &amp; ( for n being Nat holds b3 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) );

theorem Th16: :: PROB_3:16
for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n &amp; ( for k being Nat st k < n holds
not x in A1 . k ) ) )
proofend;

theorem Th17: :: PROB_3:17
for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n
proofend;

theorem Th18: :: PROB_3:18
for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
proofend;

theorem Th19: :: PROB_3:19
for X being set
for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
proofend;

theorem Th20: :: PROB_3:20
for X being set
for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1
proofend;

definition
let X be set ;
let A1 be SetSequence of X;
:: original:disjoint_valued
redefine attrA1 is disjoint_valued  means :Def4: :: PROB_3:def 4
 for m, n being Nat st m <> n holds
A1 . m misses A1 . n;
compatibility
 ( A1 is disjoint_valued iff for m, n being Nat st m <> n holds
A1 . m misses A1 . n )
proofend;
end;

:: deftheorem Def4 defines disjoint_valued PROB_3:def_4_:_
 for X being set
for A1 being SetSequence of X holds
( A1 is disjoint_valued iff for m, n being Nat st m <> n holds
A1 . m misses A1 . n );

registration
let X be set ;
let A1 be SetSequence of X;
cluster Partial_Diff_Union A1 -> V73() ;
coherence
 Partial_Diff_Union A1 is disjoint_valued
proofend;
end;

registration
let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
cluster Partial_Intersection XSeq -> Si -valued ;
coherence
 Partial_Intersection XSeq is Si -valued
proofend;
end;

registration
let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
cluster Partial_Union XSeq -> Si -valued ;
coherence
 Partial_Union XSeq is Si -valued
proofend;
end;

registration
let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
cluster Partial_Diff_Union XSeq -> Si -valued ;
coherence
 Partial_Diff_Union XSeq is Si -valued
proofend;
end;

theorem :: PROB_3:21
for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Intersection XSeq holds
( YSeq . 0 = XSeq . 0 &amp; ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) /\ (XSeq . (n + 1)) ) ) by Def1;

theorem :: PROB_3:22
for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Union XSeq holds
( YSeq . 0 = XSeq . 0 &amp; ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) \/ (XSeq . (n + 1)) ) ) by Def2;

theorem :: PROB_3:23
for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Intersection XSeq) . n c= XSeq . n by Th8;

theorem :: PROB_3:24
for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds XSeq . n c= (Partial_Union XSeq) . n by Th9;

theorem :: PROB_3:25
for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds
x in XSeq . k ) by Th12;

theorem :: PROB_3:26
for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n &amp; x in XSeq . k ) ) by Th13;

theorem :: PROB_3:27
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Intersection XSeq is V70() by Th10;

theorem :: PROB_3:28
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Union XSeq is V71() by Th11;

theorem :: PROB_3:29
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Intersection (Partial_Intersection XSeq) = Intersection XSeq by Th14;

theorem :: PROB_3:30
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (Partial_Union XSeq) = Union XSeq by Th15;

theorem :: PROB_3:31
for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Diff_Union XSeq holds
( YSeq . 0 = XSeq . 0 &amp; ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((Partial_Union XSeq) . n) ) ) by Def3;

theorem :: PROB_3:32
for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n &amp; ( for k being Nat st k < n holds
not x in XSeq . k ) ) ) by Th16;

theorem :: PROB_3:33
for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= XSeq . n by Th17;

theorem :: PROB_3:34
for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18;

theorem :: PROB_3:35
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19;

theorem :: PROB_3:36
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20;

theorem Th37: :: PROB_3:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing
proofend;

theorem :: PROB_3:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing
proofend;

theorem :: PROB_3:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing
proofend;

theorem Th40: :: PROB_3:40
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0
proofend;

theorem Th41: :: PROB_3:41
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( P * (Partial_Union ASeq) is convergent &amp; lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) &amp; lim (P * (Partial_Union ASeq)) = P . (Union ASeq) )
proofend;

theorem Th42: :: PROB_3:42
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma st ASeq is V73() holds
for n, m being Nat st n < m holds
(Partial_Union ASeq) . n misses ASeq . m
proofend;

theorem Th43: :: PROB_3:43
for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V73() holds
(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n
proofend;

theorem Th44: :: PROB_3:44
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V73() holds
P * (Partial_Union ASeq) = Partial_Sums (P * ASeq)
proofend;

theorem Th45: :: PROB_3:45
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V73() holds
( Partial_Sums (P * ASeq) is convergent &amp; lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) &amp; lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )
proofend;

theorem Th46: :: PROB_3:46
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is V73() holds
P . (Union ASeq) = Sum (P * ASeq)
proofend;

definition
let X be set ;
let F1 be FinSequence of bool X;
let n be Nat;
:: original:.
redefine funcF1 . n ->  Subset of X;
coherence
 F1 . n is Subset of X
proofend;
end;

theorem :: PROB_3:47
for X being set ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X
proofend;

theorem :: PROB_3:48
for X being set
for F1 being FinSequence of bool X holds union (rng F1) is Subset of X ;

definition
let X be set ;
let F1 be FinSequence of bool X;
:: original:Union
redefine func Union F1 ->  Subset of X;
coherence
 Union F1 is Subset of X
proofend;
end;

theorem Th49: :: PROB_3:49
for X, x being set
for F1 being FinSequence of bool X holds
( x in Union F1 iff ex k being Nat st
( k in dom F1 &amp; x in F1 . k ) )
proofend;

definition
let X be set ;
let F1 be FinSequence of bool X;
func Complement F1 ->  FinSequence of bool X means :Def5: :: PROB_3:def 5
( len it = len F1 &amp; ( for n being Nat st n in dom it holds
it . n = (F1 . n) ` ) );
existence
 ex b1 being FinSequence of bool X st
( len b1 = len F1 &amp; ( for n being Nat st n in dom b1 holds
b1 . n = (F1 . n) ` ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of bool X st len b1 = len F1 &amp; ( for n being Nat st n in dom b1 holds
b1 . n = (F1 . n) ` ) &amp; len b2 = len F1 &amp; ( for n being Nat st n in dom b2 holds
b2 . n = (F1 . n) ` ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Complement PROB_3:def_5_:_
 for X being set
for F1, b3 being FinSequence of bool X holds
( b3 = Complement F1 iff ( len b3 = len F1 &amp; ( for n being Nat st n in dom b3 holds
b3 . n = (F1 . n) ` ) ) );

definition
let X be set ;
let F1 be FinSequence of bool X;
func Intersection F1 ->  Subset of X equals :Def6: :: PROB_3:def 6
(Union (Complement F1)) `  if F1 <> {}
otherwise  {} ;
coherence
 ( ( F1 <> {} implies (Union (Complement F1)) ` is Subset of X ) &amp; ( not F1 <> {} implies {} is Subset of X ) ) by SUBSET_1:1;
consistency
 for b1 being Subset of X holds verum ;
end;

:: deftheorem Def6 defines Intersection PROB_3:def_6_:_
 for X being set
for F1 being FinSequence of bool X holds
( ( F1 <> {} implies Intersection F1 = (Union (Complement F1)) ` ) &amp; ( not F1 <> {} implies Intersection F1 = {} ) );

theorem Th50: :: PROB_3:50
for X being set
for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1
proofend;

theorem Th51: :: PROB_3:51
for X, x being set
for F1 being FinSequence of bool X st F1 <> {} holds
( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )
proofend;

theorem Th52: :: PROB_3:52
for X, x being set
for F1 being FinSequence of bool X st F1 <> {} holds
( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n )
proofend;

theorem :: PROB_3:53
for X being set
for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)
proofend;

theorem Th54: :: PROB_3:54
for X being set
for F1 being FinSequence of bool X ex A1 being SetSequence of X st
( ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) &amp; ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) )
proofend;

theorem Th55: :: PROB_3:55
for X being set
for F1 being FinSequence of bool X
for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) &amp; ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) holds
( A1 . 0 = {} &amp; Union A1 = Union F1 )
proofend;

definition
let X be set ;
let Si be SigmaField of X;
:: original:FinSequence
redefine mode FinSequence of Si ->  FinSequence of bool X;
coherence
 for b1 being FinSequence of Si holds b1 is FinSequence of bool X
proofend;
end;

definition
let X be set ;
let Si be SigmaField of X;
let FSi be FinSequence of Si;
let n be Nat;
:: original:.
redefine funcFSi . n ->  Event of Si;
coherence
 FSi . n is Event of Si
proofend;
end;

theorem Th56: :: PROB_3:56
for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si ex ASeq being SetSequence of Si st
( ( for k being Nat st k in dom FSi holds
ASeq . k = FSi . k ) &amp; ( for k being Nat st not k in dom FSi holds
ASeq . k = {} ) )
proofend;

theorem Th57: :: PROB_3:57
for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Union FSi in Si
proofend;

registration
let X be set ;
let S be SigmaField of X;
let F be FinSequence of S;
cluster Complement F -> S -valued ;
coherence
 Complement F is S -valued
proofend;
end;

theorem :: PROB_3:58
for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Intersection FSi in Si
proofend;

theorem Th59: :: PROB_3:59
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq
proofend;

theorem Th60: :: PROB_3:60
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let FSeq be FinSequence of Sigma;
let P be Probability of Sigma;
:: original:*
redefine funcP * FSeq ->  FinSequence of REAL ;
coherence
 FSeq * P is FinSequence of REAL by Th60;
end;

theorem Th61: :: PROB_3:61
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq
proofend;

theorem Th62: :: PROB_3:62
for RFin being FinSequence of REAL st len RFin = 0 holds
Sum RFin = 0
proofend;

theorem Th63: :: PROB_3:63
for RFin being FinSequence of REAL st len RFin >= 1 holds
ex f being Real_Sequence st
( f . 1 = RFin . 1 &amp; ( for n being Nat st 0 <> n &amp; n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) &amp; Sum RFin = f . (len RFin) )
proofend;

theorem Th64: :: PROB_3:64
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma
for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k ) &amp; ( for k being Nat st not k in dom FSeq holds
ASeq . k = {} ) holds
( Partial_Sums (P * ASeq) is convergent &amp; Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) &amp; P . (Union ASeq) <= Sum (P * ASeq) &amp; Sum (P * FSeq) = Sum (P * ASeq) )
proofend;

theorem :: PROB_3:65
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) &amp; ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )
proofend;

definition
canceled;
canceled;
let X be set ;
let IT be Subset-Family of X;
attrIT is non-decreasing-closed  means :Def9: :: PROB_3:def 9
 for A1 being SetSequence of X st A1 is V71() &amp; rng A1 c= IT holds
Union A1 in IT;
attrIT is non-increasing-closed  means :Def10: :: PROB_3:def 10
 for A1 being SetSequence of X st A1 is V70() &amp; rng A1 c= IT holds
Intersection A1 in IT;
end;

:: deftheorem  PROB_3:def_7_:_
canceled;

:: deftheorem  PROB_3:def_8_:_
canceled;

:: deftheorem Def9 defines non-decreasing-closed PROB_3:def_9_:_
 for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() &amp; rng A1 c= IT holds
Union A1 in IT );

:: deftheorem Def10 defines non-increasing-closed PROB_3:def_10_:_
 for X being set
for IT being Subset-Family of X holds
( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() &amp; rng A1 c= IT holds
Intersection A1 in IT );

theorem Th66: :: PROB_3:66
for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() &amp; rng A1 c= IT holds
lim A1 in IT )
proofend;

theorem Th67: :: PROB_3:67
for X being set
for IT being Subset-Family of X holds
( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() &amp; rng A1 c= IT holds
lim A1 in IT )
proofend;

theorem Th68: :: PROB_3:68
for X being set holds
( bool X is non-decreasing-closed &amp; bool X is non-increasing-closed )
proofend;

registration
let X be set ;
cluster non-decreasing-closed non-increasing-closed for Element of K10(K10(X));
existence
 ex b1 being Subset-Family of X st
( b1 is non-decreasing-closed &amp; b1 is non-increasing-closed )
proofend;
end;

definition
let X be set ;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;
end;

theorem Th69: :: PROB_3:69
for Z, X being set holds
( Z is MonotoneClass of X iff ( Z c= bool X &amp; ( for A1 being SetSequence of X st A1 is monotone &amp; rng A1 c= Z holds
lim A1 in Z ) ) )
proofend;

theorem Th70: :: PROB_3:70
for X being set
for F being Field_Subset of X holds
( F is SigmaField of X iff F is MonotoneClass of X )
proofend;

theorem :: PROB_3:71
for Omega being non empty set holds bool Omega is MonotoneClass of Omega by Th68;

definition
let Omega be non empty set ;
let X be Subset-Family of Omega;
func monotoneclass X ->  MonotoneClass of Omega means :Def11: :: PROB_3:def 11
( X c= it &amp; ( for Z being set st X c= Z &amp; Z is MonotoneClass of Omega holds
it c= Z ) );
existence
 ex b1 being MonotoneClass of Omega st
( X c= b1 &amp; ( for Z being set st X c= Z &amp; Z is MonotoneClass of Omega holds
b1 c= Z ) )
proofend;
uniqueness
 for b1, b2 being MonotoneClass of Omega st X c= b1 &amp; ( for Z being set st X c= Z &amp; Z is MonotoneClass of Omega holds
b1 c= Z ) &amp; X c= b2 &amp; ( for Z being set st X c= Z &amp; Z is MonotoneClass of Omega holds
b2 c= Z ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines monotoneclass PROB_3:def_11_:_
 for Omega being non empty set
for X being Subset-Family of Omega
for b3 being MonotoneClass of Omega holds
( b3 = monotoneclass X iff ( X c= b3 &amp; ( for Z being set st X c= Z &amp; Z is MonotoneClass of Omega holds
b3 c= Z ) ) );

theorem Th72: :: PROB_3:72
for Omega being non empty set
for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega
proofend;

theorem :: PROB_3:73
for Omega being non empty set
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
proofend;