:: PROB_1 semantic presentation

begin


theorem Th1: :: PROB_1:1
for r being real number
for seq being Real_Sequence st ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )
let seq be Real_Sequence; ::_thesis: ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r implies ( seq is convergent & lim seq = r ) )
assume A1: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r ; ::_thesis: ( seq is convergent & lim seq = r )
A2: for r1 being real number st 0 < r1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1
proof
consider n being Element of NAT  such that
A3: for m being Element of NAT st n <= m holds
seq . m = r by A1;
let r1 be real number ; ::_thesis: ( 0 < r1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1 )
assume A4: 0 < r1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - r) < r1 )
assume  n <= m ; ::_thesis: abs ((seq . m) - r) < r1
then  seq . m = r by A3;
hence  abs ((seq . m) - r) < r1 by A4, ABSVALUE:2; ::_thesis: verum
end;
then  seq is convergent by SEQ_2:def_6;
hence  ( seq is convergent & lim seq = r ) by A2, SEQ_2:def_7; ::_thesis: verum
end;

definition
let X be set ;
let IT be Subset-Family of X;
attrIT is compl-closed  means :Def1: :: PROB_1:def 1
 for A being Subset of X st A in IT holds
A ` in IT;
end;

:: deftheorem Def1 defines compl-closed PROB_1:def_1_:_
 for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being Subset of X st A in IT holds
A ` in IT );

registration
let X be set ;
cluster bool X ->  cap-closed ;
coherence
 bool X is cap-closed
proof
let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in bool X or not B in bool X or A /\ B in bool X )
assume that
A1: A in bool X and
 B in bool X ; ::_thesis: A /\ B in bool X
 A /\ B c= X by A1, XBOOLE_1:108;
hence  A /\ B in bool X ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster bool X ->  compl-closed for Subset-Family of X;
coherence
 for b1 being Subset-Family of X st b1 = bool X holds
b1 is compl-closed
proof
 bool X is compl-closed
proof
let A be Subset of X; :: according to PROB_1:def_1 ::_thesis: ( A in bool X implies A ` in bool X )
thus  ( A in bool X implies A ` in bool X ) ; ::_thesis: verum
end;
hence  for b1 being Subset-Family of X st b1 = bool X holds
b1 is compl-closed ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster non empty cap-closed compl-closed for Event of ;
existence
 ex b1 being Subset-Family of X st
( not b1 is empty & b1 is compl-closed & b1 is cap-closed )
proof
take  bool X ; ::_thesis: ( not bool X is empty & bool X is compl-closed & bool X is cap-closed )
thus  ( not bool X is empty & bool X is compl-closed & bool X is cap-closed ) ; ::_thesis: verum
end;
end;

definition
let X be set ;
mode Field_Subset of X is non empty cap-closed compl-closed Subset-Family of X;
end;

theorem Th2: :: PROB_1:2
for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X
proof
let X be set ; ::_thesis: for A, B being Subset of X holds {A,B} is Subset-Family of X
let A, B be Subset of X; ::_thesis: {A,B} is Subset-Family of X
set C = {A,B};
 {A,B} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,B} or x in bool X )
assume  x in {A,B} ; ::_thesis: x in bool X
then  ( x = A or x = B ) by TARSKI:def_2;
hence  x in bool X ; ::_thesis: verum
end;
hence  {A,B} is Subset-Family of X ; ::_thesis: verum
end;

theorem Th3: :: PROB_1:3
for X being set
for F being Field_Subset of X
for A, B being set st A in F & B in F holds
A \/ B in F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for A, B being set st A in F & B in F holds
A \/ B in F
let F be Field_Subset of X; ::_thesis: for A, B being set st A in F & B in F holds
A \/ B in F
let A, B be set ; ::_thesis: ( A in F & B in F implies A \/ B in F )
assume A1: ( A in F & B in F ) ; ::_thesis: A \/ B in F
then reconsider A1 = A, B1 = B as Subset of X ;
 ( A1 ` in F & B1 ` in F ) by A1, Def1;
then  (A1 `) /\ (B1 `) in F by FINSUB_1:def_2;
then  (A1 \/ B1) ` in F by XBOOLE_1:53;
then  ((A1 \/ B1) `) ` in F by Def1;
hence  A \/ B in F ; ::_thesis: verum
end;

theorem Th4: :: PROB_1:4
for X being set
for F being Field_Subset of X holds {} in F
proof
let X be set ; ::_thesis: for F being Field_Subset of X holds {} in F
let F be Field_Subset of X; ::_thesis: {} in F
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
 A misses A ` by XBOOLE_1:79;
then A2: A /\ (A `) = {} by XBOOLE_0:def_7;
 A ` in F by A1, Def1;
hence  {} in F by A1, A2, FINSUB_1:def_2; ::_thesis: verum
end;

theorem Th5: :: PROB_1:5
for X being set
for F being Field_Subset of X holds X in F
proof
let X be set ; ::_thesis: for F being Field_Subset of X holds X in F
let F be Field_Subset of X; ::_thesis: X in F
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
A2: A \/ (A `) = [#] X by SUBSET_1:10
.= X ;
 A ` in F by A1, Def1;
hence  X in F by A1, A2, Th3; ::_thesis: verum
end;

theorem Th6: :: PROB_1:6
for X being set
for F being Field_Subset of X
for A, B being Subset of X st A in F & B in F holds
A \ B in F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for A, B being Subset of X st A in F & B in F holds
A \ B in F
let F be Field_Subset of X; ::_thesis: for A, B being Subset of X st A in F & B in F holds
A \ B in F
let A, B be Subset of X; ::_thesis: ( A in F & B in F implies A \ B in F )
assume A1: A in F ; ::_thesis: ( not B in F or A \ B in F )
assume  B in F ; ::_thesis: A \ B in F
then  B ` in F by Def1;
then  A /\ (B `) in F by A1, FINSUB_1:def_2;
hence  A \ B in F by SUBSET_1:13; ::_thesis: verum
end;

theorem :: PROB_1:7
for X being set
for F being Field_Subset of X
for A, B being set st A in F & B in F holds
(A \ B) \/ B in F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for A, B being set st A in F & B in F holds
(A \ B) \/ B in F
let F be Field_Subset of X; ::_thesis: for A, B being set st A in F & B in F holds
(A \ B) \/ B in F
let A, B be set ; ::_thesis: ( A in F & B in F implies (A \ B) \/ B in F )
 A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence  ( A in F & B in F implies (A \ B) \/ B in F ) by Th3; ::_thesis: verum
end;

registration
let X be set ;
cluster{{},X} ->  cap-closed ;
coherence
 {{},X} is cap-closed
proof
let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} )
A1: ( ( A = {} or B = {} ) implies A /\ B = {} ) ;
 ( A = X & B = X implies A /\ B = X ) ;
hence  ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} ) by A1, TARSKI:def_2; ::_thesis: verum
end;
end;

theorem :: PROB_1:8
for X being set holds {{},X} is Field_Subset of X
proof
let X be set ; ::_thesis: {{},X} is Field_Subset of X
 ( {} c= X & X in bool X ) by XBOOLE_1:2, ZFMISC_1:def_1;
then reconsider EX = {{},X} as Subset-Family of X by Th2;
now__::_thesis:_for_A_being_Subset_of_X_st_A_in_EX_holds_
A_`_in_EX
let A be Subset of X; ::_thesis: ( A in EX implies A ` in EX )
A1: ( A = {} implies A ` = X ) ;
 ( A = X implies A ` = {} X ) by XBOOLE_1:37;
hence  ( A in EX implies A ` in EX ) by A1, TARSKI:def_2; ::_thesis: verum
end;
hence  {{},X} is Field_Subset of X by Def1; ::_thesis: verum
end;

theorem :: PROB_1:9
for X being set holds bool X is Field_Subset of X ;

theorem :: PROB_1:10
for X being set
for F being Field_Subset of X holds
( {{},X} c= F & F c= bool X )
proof
let X be set ; ::_thesis: for F being Field_Subset of X holds
( {{},X} c= F & F c= bool X )
let F be Field_Subset of X; ::_thesis: ( {{},X} c= F & F c= bool X )
 ( {} in F & X in F ) by Th4, Th5;
then  for x being set st x in {{},X} holds
x in F by TARSKI:def_2;
hence  ( {{},X} c= F & F c= bool X ) by TARSKI:def_3; ::_thesis: verum
end;

definition
let X be set ;
mode SetSequence of X is sequence of (bool X);
end;


theorem Th11: :: PROB_1:11
for X being set
for A1 being SetSequence of X holds union (rng A1) is Subset of X
proof
let X be set ; ::_thesis: for A1 being SetSequence of X holds union (rng A1) is Subset of X
let A1 be SetSequence of X; ::_thesis: union (rng A1) is Subset of X
 for Y being set st Y in rng A1 holds
Y c= X
proof
let Y be set ; ::_thesis: ( Y in rng A1 implies Y c= X )
assume  Y in rng A1 ; ::_thesis: Y c= X
then consider y being set  such that
A1: y in dom A1 and
A2: Y = A1 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A1, FUNCT_2:def_1;
 Y = A1 . y by A2;
hence  Y c= X ; ::_thesis: verum
end;
hence  union (rng A1) is Subset of X by ZFMISC_1:76; ::_thesis: verum
end;

definition
let X be set ;
let A1 be SetSequence of X;
:: original: Union
redefine func Union A1 ->  Subset of X;
coherence
 Union A1 is Subset of X by Th11;
end;

theorem Th12: :: PROB_1:12
for X, x being set
for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Element of NAT st x in A1 . n )
proof
let X, x be set ; ::_thesis: for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Element of NAT st x in A1 . n )
let A1 be SetSequence of X; ::_thesis: ( x in Union A1 iff ex n being Element of NAT st x in A1 . n )
set DX = union (rng A1);
 for x being set holds
( x in union (rng A1) iff ex n being Element of NAT st x in A1 . n )
proof
let x be set ; ::_thesis: ( x in union (rng A1) iff ex n being Element of NAT st x in A1 . n )
thus  ( x in union (rng A1) implies ex n being Element of NAT st x in A1 . n ) ::_thesis: ( ex n being Element of NAT st x in A1 . n implies x in union (rng A1) )
proof
assume  x in union (rng A1) ; ::_thesis: ex n being Element of NAT st x in A1 . n
then consider Y being set  such that
A1: x in Y and
A2: Y in rng A1 by TARSKI:def_4;
consider p being set  such that
A3: p in dom A1 and
A4: Y = A1 . p by A2, FUNCT_1:def_3;
 p in NAT by A3, FUNCT_2:def_1;
hence  ex n being Element of NAT st x in A1 . n by A1, A4; ::_thesis: verum
end;
thus  ( ex n being Element of NAT st x in A1 . n implies x in union (rng A1) ) ::_thesis: verum
proof
given n being Element of NAT  such that A5: x in A1 . n ; ::_thesis: x in union (rng A1)
 n in NAT ;
then  n in dom A1 by FUNCT_2:def_1;
then  A1 . n in rng A1 by FUNCT_1:def_3;
hence  x in union (rng A1) by A5, TARSKI:def_4; ::_thesis: verum
end;
end;
hence  ( x in Union A1 iff ex n being Element of NAT st x in A1 . n ) ; ::_thesis: verum
end;

definition
let X be set ;
let A1 be SetSequence of X;
func Complement A1 ->  SetSequence of X means :Def2: :: PROB_1:def 2
 for n being Element of NAT holds it . n = (A1 . n) ` ;
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) `
proof
deffunc H1( Element of NAT ) ->  Event of = (A1 . $1) ` ;
 ex f being Function of NAT,(bool X) st
for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_4();
then consider f being Function of NAT,(bool X) such that
A1: for x being Element of NAT holds f . x = (A1 . x) ` ;
take  f ; ::_thesis: for n being Element of NAT holds f . n = (A1 . n) `
thus  for n being Element of NAT holds f . n = (A1 . n) ` by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) ` ) & ( for n being Element of NAT holds b2 . n = (A1 . n) ` ) holds
b1 = b2
proof
let BSeq, CSeq be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds BSeq . n = (A1 . n) ` ) & ( for n being Element of NAT holds CSeq . n = (A1 . n) ` ) implies BSeq = CSeq )
assume that
A2: for n being Element of NAT holds BSeq . n = (A1 . n) ` and
A3: for m being Element of NAT holds CSeq . m = (A1 . m) ` ; ::_thesis: BSeq = CSeq
A4: for x being set st x in NAT holds
BSeq . x = CSeq . x
proof
let x be set ; ::_thesis: ( x in NAT implies BSeq . x = CSeq . x )
assume  x in NAT ; ::_thesis: BSeq . x = CSeq . x
then reconsider x = x as Element of NAT ;
BSeq . x = (A1 . x) ` by A2
.= CSeq . x by A3 ;
hence  BSeq . x = CSeq . x ; ::_thesis: verum
end;
 ( NAT = dom BSeq & NAT = dom CSeq ) by FUNCT_2:def_1;
hence  BSeq = CSeq by A4, FUNCT_1:2; ::_thesis: verum
end;
involutiveness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (b2 . n) ` ) holds
for n being Element of NAT holds b2 . n = (b1 . n) `
proof
let IT, A1 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds IT . n = (A1 . n) ` ) implies for n being Element of NAT holds A1 . n = (IT . n) ` )
assume A5: for n being Element of NAT holds IT . n = (A1 . n) ` ; ::_thesis: for n being Element of NAT holds A1 . n = (IT . n) `
let n be Element of NAT ; ::_thesis: A1 . n = (IT . n) `
thus A1 . n = ((A1 . n) `) `
.= (IT . n) ` by A5 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Complement PROB_1:def_2_:_
 for X being set
for A1, b3 being SetSequence of X holds
( b3 = Complement A1 iff for n being Element of NAT holds b3 . n = (A1 . n) ` );

definition
let X be set ;
let A1 be SetSequence of X;
func Intersection A1 ->  Subset of X equals :: PROB_1:def 3
(Union (Complement A1)) ` ;
correctness
coherence
(Union (Complement A1)) ` is Subset of X;
;
end;

:: deftheorem  defines Intersection PROB_1:def_3_:_
 for X being set
for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ;

theorem Th13: :: PROB_1:13
for X, x being set
for A1 being SetSequence of X holds
( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
proof
let X, x be set ; ::_thesis: for A1 being SetSequence of X holds
( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
let A1 be SetSequence of X; ::_thesis: ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
A1: for n being Element of NAT holds X \ ((Complement A1) . n) = A1 . n
proof
let n be Element of NAT ; ::_thesis: X \ ((Complement A1) . n) = A1 . n
X \ ((Complement A1) . n) = ((A1 . n) `) ` by Def2
.= A1 . n ;
hence  X \ ((Complement A1) . n) = A1 . n ; ::_thesis: verum
end;
A2: ( ( for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ) iff for n being Element of NAT holds x in A1 . n )
proof
thus  ( ( for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ) implies for n being Element of NAT holds x in A1 . n ) ::_thesis: ( ( for n being Element of NAT holds x in A1 . n ) implies for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) )
proof
assume A3: for n being Element of NAT holds
( x in X & not x in (Complement A1) . n ) ; ::_thesis: for n being Element of NAT holds x in A1 . n
let n be Element of NAT ; ::_thesis: x in A1 . n
 not x in (Complement A1) . n by A3;
then  x in X \ ((Complement A1) . n) by A3, XBOOLE_0:def_5;
hence  x in A1 . n by A1; ::_thesis: verum
end;
assume A4: for n being Element of NAT holds x in A1 . n ; ::_thesis: for n being Element of NAT holds
( x in X & not x in (Complement A1) . n )
let n be Element of NAT ; ::_thesis: ( x in X & not x in (Complement A1) . n )
 x in A1 . n by A4;
then  x in X \ ((Complement A1) . n) by A1;
hence  ( x in X & not x in (Complement A1) . n ) by XBOOLE_0:def_5; ::_thesis: verum
end;
 ( x in X & not x in Union (Complement A1) iff ( x in X & ( for n being Element of NAT holds not x in (Complement A1) . n ) ) ) by Th12;
hence  ( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n ) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

Lm1:  for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
proof
let X be set ; ::_thesis: for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
let A, B be Subset of X; ::_thesis: Complement (A followed_by B) = (A `) followed_by (B `)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n
percases ( n = 0 or n > 0 ) by NAT_1:3;
supposeA1: n = 0 ; ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n
thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2
.= A ` by A1, FUNCT_7:119
.= ((A `) followed_by (B `)) . n by A1, FUNCT_7:119 ; ::_thesis: verum
end;
supposeA2: n > 0 ; ::_thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n
thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2
.= B ` by A2, FUNCT_7:120
.= ((A `) followed_by (B `)) . n by A2, FUNCT_7:120 ; ::_thesis: verum
end;
end;
end;

theorem Th14: :: PROB_1:14
for X being set
for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B
proof
let X be set ; ::_thesis: for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B
let A, B be Subset of X; ::_thesis: Intersection (A followed_by B) = A /\ B
set A1 = A followed_by B;
 Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;
then  rng (Complement (A followed_by B)) = {(A `),(B `)} by FUNCT_7:126;
then  Union (Complement (A followed_by B)) = (A `) \/ (B `) by ZFMISC_1:75;
then  (Union (Complement (A followed_by B))) ` = ((A `) `) /\ ((B `) `) by XBOOLE_1:53;
hence  Intersection (A followed_by B) = A /\ B ; ::_thesis: verum
end;

definition
let f be Function;
attrf is non-ascending  means :Def4: :: PROB_1:def 4
 for n, m being Element of NAT st n <= m holds
f . m c= f . n;
attrf is non-descending  means :: PROB_1:def 5
 for n, m being Element of NAT st n <= m holds
f . n c= f . m;
end;

:: deftheorem Def4 defines non-ascending PROB_1:def_4_:_
 for f being Function holds
( f is non-ascending iff for n, m being Element of NAT st n <= m holds
f . m c= f . n );

:: deftheorem  defines non-descending PROB_1:def_5_:_
 for f being Function holds
( f is non-descending iff for n, m being Element of NAT st n <= m holds
f . n c= f . m );

definition
let X be set ;
let F be Subset-Family of X;
attrF is sigma-multiplicative  means :Def6: :: PROB_1:def 6
 for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F;
end;

:: deftheorem Def6 defines sigma-multiplicative PROB_1:def_6_:_
 for X being set
for F being Subset-Family of X holds
( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F );

registration
let X be set ;
cluster bool X ->  sigma-multiplicative for Subset-Family of X;
coherence
 for b1 being Subset-Family of X st b1 = bool X holds
b1 is sigma-multiplicative
proof
 for BSeq being SetSequence of X st rng BSeq c= bool X holds
Intersection BSeq in bool X ;
hence  for b1 being Subset-Family of X st b1 = bool X holds
b1 is sigma-multiplicative by Def6; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative for Event of ;
existence
 ex b1 being Subset-Family of X st
( b1 is compl-closed & b1 is sigma-multiplicative & not b1 is empty )
proof
take  bool X ; ::_thesis: ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty )
thus  ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty ) ; ::_thesis: verum
end;
end;

definition
let X be set ;
mode SigmaField of X is non empty compl-closed sigma-multiplicative Subset-Family of X;
end;

theorem :: PROB_1:15
for X being set
for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Intersection A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ) by Def1, Def6;

theorem Th16: :: PROB_1:16
for Y, X being set st Y is SigmaField of X holds
Y is Field_Subset of X
proof
let Y, X 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
end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative  ->  cap-closed for Event of ;
coherence
 for b1 being SigmaField of X holds
( b1 is cap-closed & b1 is compl-closed ) by Th16;
end;


registration
let X be set ;
let F be non empty Subset-Family of X;
cluster Relation-like NAT -defined F -valued bool X -valued Function-like V37( NAT , bool X) for Event of ;
existence
 ex b1 being SetSequence of X st b1 is F -valued
proof
set A1 = NAT --> the Element of F;
reconsider A1 = NAT --> the Element of F as SetSequence of X by FUNCOP_1:45;
take  A1 ; ::_thesis: A1 is F -valued
thus  A1 is F -valued ; ::_thesis: verum
end;
end;

definition
let X be set ;
let F be non empty Subset-Family of X;
mode SetSequence of F is F -valued SetSequence of X;
end;

theorem Th17: :: PROB_1:17
for X being set
for Si being SigmaField of X
for ASeq being SetSequence of Si holds Union ASeq in Si
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for ASeq being SetSequence of Si holds Union ASeq in Si
let Si be SigmaField of X; ::_thesis: for ASeq being SetSequence of Si holds Union ASeq in Si
let ASeq be SetSequence of Si; ::_thesis: Union ASeq in Si
A1: for A1 being SetSequence of X st rng A1 c= Si holds
for n being Nat holds (Complement A1) . n in Si
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies for n being Nat holds (Complement A1) . n in Si )
assume A2: rng A1 c= Si ; ::_thesis: for n being Nat holds (Complement A1) . n in Si
let n be Nat; ::_thesis: (Complement A1) . n in Si
 A1 . n in rng A1 by NAT_1:51;
then  ( n in NAT & (A1 . n) ` in Si ) by A2, Def1, ORDINAL1:def_12;
hence  (Complement A1) . n in Si by Def2; ::_thesis: verum
end;
A3: for A1 being SetSequence of X st rng A1 c= Si holds
Union (Complement (Complement A1)) in Si
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies Union (Complement (Complement A1)) in Si )
assume  rng A1 c= Si ; ::_thesis: Union (Complement (Complement A1)) in Si
then  for n being Nat holds (Complement A1) . n in Si by A1;
then  rng (Complement A1) c= Si by NAT_1:52;
then  Intersection (Complement A1) in Si by Def6;
then  ((Union (Complement (Complement A1))) `) ` in Si by Def1;
hence  Union (Complement (Complement A1)) in Si ; ::_thesis: verum
end;
A4: for A1 being SetSequence of X st rng A1 c= Si holds
Union A1 in Si
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= Si implies Union A1 in Si )
assume  rng A1 c= Si ; ::_thesis: Union A1 in Si
then  Union (Complement (Complement A1)) in Si by A3;
hence  Union A1 in Si ; ::_thesis: verum
end;
 rng ASeq c= Si by RELAT_1:def_19;
hence  Union ASeq in Si by A4; ::_thesis: verum
end;

notation
let X be set ;
let F be SigmaField of X;
synonym  Event of F for  Element of X;
end;

definition
let X be set ;
let F be SigmaField of X;
:: original: Event
redefine mode Event of F ->  Subset of X;
coherence
 for b1 being Event of holds b1 is Subset of X
proof
let E be Event of ; ::_thesis: E is Subset of X
 E in F ;
hence  E is Subset of X ; ::_thesis: verum
end;
end;

theorem :: PROB_1:18
for X, x being set
for Si being SigmaField of X st x in Si holds
x is Event of Si ;

theorem :: PROB_1:19
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def_2;

theorem :: PROB_1:20
for X being set
for Si being SigmaField of X
for A being Event of Si holds A ` is Event of Si by Def1;

theorem :: PROB_1:21
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \/ B is Event of Si by Th3;

theorem :: PROB_1:22
for X being set
for Si being SigmaField of X holds {} is Event of Si by Th4;

theorem :: PROB_1:23
for X being set
for Si being SigmaField of X holds X is Event of Si by Th5;

theorem :: PROB_1:24
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \ B is Event of Si by Th6;

registration
let X be set ;
let Si be SigmaField of X;
cluster empty for Event of ;
existence
 ex b1 being Event of Si st b1 is empty
proof
 {} is Event of Si by Th4;
hence  ex b1 being Event of Si st b1 is empty ; ::_thesis: verum
end;
end;

definition
let X be set ;
let Si be SigmaField of X;
func [#] Si ->  Event of Si equals :: PROB_1:def 7
X;
coherence
 X is Event of Si by Th5;
end;

:: deftheorem  defines [#] PROB_1:def_7_:_
 for X being set
for Si being SigmaField of X holds [#] Si = X;

definition
let X be set ;
let Si be SigmaField of X;
let A, B be Event of Si;
:: original: /\
redefine funcA /\ B ->  Event of Si;
coherence
 A /\ B is Event of Si by FINSUB_1:def_2;
:: original: \/
redefine funcA \/ B ->  Event of Si;
coherence
 A \/ B is Event of Si by Th3;
:: original: \
redefine funcA \ B ->  Event of Si;
coherence
 A \ B is Event of Si by Th6;
end;

theorem :: PROB_1:25
for X being set
for A1 being SetSequence of X
for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )
proof
let X be set ; ::_thesis: for A1 being SetSequence of X
for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )
let A1 be SetSequence of X; ::_thesis: for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )
let Si be SigmaField of X; ::_thesis: ( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )
thus  ( A1 is SetSequence of Si implies for n being Element of NAT holds A1 . n is Event of Si ) ::_thesis: ( ( for n being Element of NAT holds A1 . n is Event of Si ) implies A1 is SetSequence of Si )
proof
assume  A1 is SetSequence of Si ; ::_thesis: for n being Element of NAT holds A1 . n is Event of Si
then A1: rng A1 c= Si by RELAT_1:def_19;
 for n being Element of NAT holds A1 . n is Event of Si
proof
let n be Element of NAT ; ::_thesis: A1 . n is Event of Si
 A1 . n in rng A1 by NAT_1:51;
hence  A1 . n is Event of Si by A1; ::_thesis: verum
end;
hence  for n being Element of NAT holds A1 . n is Event of Si ; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds A1 . n is Event of Si ; ::_thesis: A1 is SetSequence of Si
 for n being Nat holds A1 . n in Si
proof
let n be Nat; ::_thesis: A1 . n in Si
 n in NAT by ORDINAL1:def_12;
then  A1 . n is Event of Si by A2;
hence  A1 . n in Si ; ::_thesis: verum
end;
then  rng A1 c= Si by NAT_1:52;
hence  A1 is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum
end;

theorem :: PROB_1:26
for Omega being set
for ASeq being SetSequence of Omega
for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds
Union ASeq is Event of Sigma by Th17;


theorem Th27: :: PROB_1:27
for Omega, p being set
for Sigma being SigmaField of Omega ex f being Function st
( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )
proof
let Omega, p be set ; ::_thesis: for Sigma being SigmaField of Omega ex f being Function st
( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )
let Sigma be SigmaField of Omega; ::_thesis: ex f being Function st
( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )
deffunc H1( set ) ->  Element of NAT = 0 ;
deffunc H2( set ) ->  Element of NAT = 1;
defpred S1[ set ] means p in $1;
 ex f being Function st
( dom f = Sigma & ( for x being set st x in Sigma holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from PARTFUN1:sch_1();
then consider f being Function such that
A1: dom f = Sigma and
A2: for x being set st x in Sigma holds
( ( S1[x] implies f . x = 1 ) & ( not S1[x] implies f . x = 0 ) ) ;
take  f ; ::_thesis: ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )
thus  dom f = Sigma by A1; ::_thesis: for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) )
let D be Subset of Omega; ::_thesis: ( D in Sigma implies ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) )
assume A3: D in Sigma ; ::_thesis: ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) )
hence  ( p in D implies f . D = 1 ) by A2; ::_thesis: ( not p in D implies f . D = 0 )
assume  not p in D ; ::_thesis: f . D = 0
hence  f . D = 0 by A2, A3; ::_thesis: verum
end;

theorem Th28: :: PROB_1:28
for Omega, p being set
for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
proof
let Omega, p be set ; ::_thesis: for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
let Sigma be SigmaField of Omega; ::_thesis: ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
consider f being Function such that
A1: dom f = Sigma and
A2: for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) by Th27;
 rng f c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in REAL )
assume  y in rng f ; ::_thesis: y in REAL
then consider x being set  such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
reconsider x = x as Subset of Omega by A1, A3;
A5: ( not p in x implies y = 0 ) by A1, A2, A3, A4;
 ( p in x implies y = 1 ) by A1, A2, A3, A4;
hence  y in REAL by A5; ::_thesis: verum
end;
then reconsider f = f as Function of Sigma,REAL by A1, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) )
thus  for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) by A2; ::_thesis: verum
end;

theorem Th29: :: PROB_1:29
for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
proof
let Omega be set ; ::_thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let ASeq be SetSequence of Sigma; ::_thesis: for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
let P be Function of Sigma,REAL; ::_thesis: P * ASeq is Real_Sequence
 rng ASeq c= Sigma by RELAT_1:def_19;
then  rng ASeq c= dom P by FUNCT_2:def_1;
then A1: dom (P * ASeq) = dom ASeq by RELAT_1:27
.= NAT by FUNCT_2:def_1 ;
 rng (P * ASeq) c= REAL by RELAT_1:def_19;
hence  P * ASeq is Real_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
let P be Function of Sigma,REAL;
:: original: *
redefine funcP * ASeq ->  Real_Sequence;
coherence
 ASeq * P is Real_Sequence by Th29;
end;


definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
mode Probability of Sigma ->  Function of Sigma,REAL means :Def8: :: PROB_1:def 8
( ( for A being Event of Sigma holds 0 <= it . A ) & it . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
it . (A \/ B) = (it . A) + (it . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) );
existence
 ex b1 being Function of Sigma,REAL st
( ( for A being Event of Sigma holds 0 <= b1 . A ) & b1 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b1 . (A \/ B) = (b1 . A) + (b1 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b1 * ASeq is convergent & lim (b1 * ASeq) = b1 . (Intersection ASeq) ) ) )
proof
set p = the Element of Omega;
consider P being Function of Sigma,REAL such that
A1: for D being Subset of Omega st D in Sigma holds
( ( the Element of Omega in D implies P . D = 1 ) & ( not the Element of Omega in D implies P . D = 0 ) ) by Th28;
take  P ; ::_thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )
thus  for A being Event of Sigma holds 0 <= P . A by A1; ::_thesis: ( P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )
 [#] Sigma in Sigma ;
hence  P . Omega = 1 by A1; ::_thesis: ( ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) )
thus  for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ::_thesis: for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
proof
let A, B be Event of Sigma; ::_thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )
assume A2: A misses B ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
A3: ( the Element of Omega in A & not the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def_3;
A4: ( not the Element of Omega in A & the Element of Omega in B implies ( P . A = 0 & P . B = 1 ) ) by A1;
A5: ( not the Element of Omega in A & the Element of Omega in B implies the Element of Omega in A \/ B ) by XBOOLE_0:def_3;
A6: ( not the Element of Omega in A & not the Element of Omega in B implies ( P . A = 0 & P . B = 0 ) ) by A1;
A7: ( not the Element of Omega in A & not the Element of Omega in B implies not the Element of Omega in A \/ B ) by XBOOLE_0:def_3;
 ( the Element of Omega in A & not the Element of Omega in B implies ( P . A = 1 & P . B = 0 ) ) by A1;
hence  P . (A \/ B) = (P . A) + (P . B) by A1, A2, A3, A4, A5, A6, A7, XBOOLE_0:3; ::_thesis: verum
end;
let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
A8: for n being Element of NAT holds (P * ASeq) . n = P . (ASeq . n)
proof
let n be Element of NAT ; ::_thesis: (P * ASeq) . n = P . (ASeq . n)
 dom (P * ASeq) = NAT by FUNCT_2:def_1;
hence  (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12; ::_thesis: verum
end;
A9: ( ( for n being Element of NAT holds the Element of Omega in ASeq . n ) implies for n being Element of NAT holds (P * ASeq) . n = 1 )
proof
assume A10: for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: for n being Element of NAT holds (P * ASeq) . n = 1
 for n being Element of NAT holds (P * ASeq) . n = 1
proof
let n be Element of NAT ; ::_thesis: (P * ASeq) . n = 1
A11: ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19;
 the Element of Omega in ASeq . n by A10;
then  P . (ASeq . n) = 1 by A1, A11;
hence  (P * ASeq) . n = 1 by A8; ::_thesis: verum
end;
hence  for n being Element of NAT holds (P * ASeq) . n = 1 ; ::_thesis: verum
end;
assume A12: ASeq is non-ascending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
A13: ( not for n being Element of NAT holds the Element of Omega in ASeq . n implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 )
proof
assume  not for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
then consider m being Element of NAT  such that
A14: not the Element of Omega in ASeq . m ;
take  m ; ::_thesis: for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
 for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
proof
let n be Element of NAT ; ::_thesis: ( m <= n implies (P * ASeq) . n = 0 )
assume  m <= n ; ::_thesis: (P * ASeq) . n = 0
then  ASeq . n c= ASeq . m by A12, Def4;
then A15: not the Element of Omega in ASeq . n by A14;
 ( rng ASeq c= Sigma & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19;
then  P . (ASeq . n) = 0 by A1, A15;
hence  (P * ASeq) . n = 0 by A8; ::_thesis: verum
end;
hence  for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 ; ::_thesis: verum
end;
A16: ( ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 implies ( P * ASeq is convergent & lim (P * ASeq) = 0 ) ) by Th1;
 rng ASeq c= Sigma by RELAT_1:def_19;
then A17: Intersection ASeq in Sigma by Def6;
reconsider r = 1 as Real ;
A18: ( ( for n being Element of NAT holds (P * ASeq) . n = 1 ) implies ( P * ASeq is convergent & lim (P * ASeq) = 1 ) )
proof
assume A19: for n being Element of NAT holds (P * ASeq) . n = 1 ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = 1 )
 ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = r
proof
take  0 ; ::_thesis: for n being Element of NAT st 0 <= n holds
(P * ASeq) . n = r
thus  for n being Element of NAT st 0 <= n holds
(P * ASeq) . n = r by A19; ::_thesis: verum
end;
hence  ( P * ASeq is convergent & lim (P * ASeq) = 1 ) by Th1; ::_thesis: verum
end;
percases ( ex n being Element of NAT st not the Element of Omega in ASeq . n or for n being Element of NAT holds the Element of Omega in ASeq . n ) ;
supposeA20: not for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then  not the Element of Omega in Intersection ASeq by Th13;
hence  ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A13, A16, A20, A17; ::_thesis: verum
end;
supposeA21: for n being Element of NAT holds the Element of Omega in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then  the Element of Omega in Intersection ASeq by Th13;
hence  ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A1, A9, A18, A21, A17; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def8 defines Probability PROB_1:def_8_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for b3 being Function of Sigma,REAL holds
( b3 is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b3 . A ) & b3 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b3 . (A \/ B) = (b3 . A) + (b3 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b3 * ASeq is convergent & lim (b3 * ASeq) = b3 . (Intersection ASeq) ) ) ) );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster  ->  zeroed for Probability of Sigma;
coherence
 for b1 being Probability of Sigma holds b1 is zeroed
proof
reconsider E = {} as Event of Sigma by Th4;
let P be Probability of Sigma; ::_thesis: P is zeroed
A1: ( {} misses [#] Sigma & {} \/ ([#] Sigma) = [#] Sigma ) by XBOOLE_1:65;
 1 = P . ([#] Sigma) by Def8;
then  1 = (P . E) + 1 by A1, Def8;
hence  P . {} = 0 ; :: according to VALUED_0:def_19 ::_thesis: verum
end;
end;

theorem :: PROB_1:30
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def8;

theorem Th31: :: PROB_1:31
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
let P be Probability of Sigma; ::_thesis: (P . (([#] Sigma) \ A)) + (P . A) = 1
A1: (([#] Sigma) \ A) \/ A = (A `) \/ A
.= [#] Omega by SUBSET_1:10
.= Omega ;
 ([#] Sigma) \ A misses A by XBOOLE_1:79;
then (P . (([#] Sigma) \ A)) + (P . A) = P . Omega by A1, Def8
.= 1 by Def8 ;
hence  (P . (([#] Sigma) \ A)) + (P . A) = 1 ; ::_thesis: verum
end;

theorem :: PROB_1:32
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)
let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma
for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)
let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)
let P be Probability of Sigma; ::_thesis: P . (([#] Sigma) \ A) = 1 - (P . A)
 (P . (([#] Sigma) \ A)) + (P . A) = 1 by Th31;
hence  P . (([#] Sigma) \ A) = 1 - (P . A) ; ::_thesis: verum
end;

theorem Th33: :: PROB_1:33
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . (B \ A) = (P . B) - (P . A)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . (B \ A) = (P . B) - (P . A)
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . (B \ A) = (P . B) - (P . A)
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A c= B holds
P . (B \ A) = (P . B) - (P . A)
let P be Probability of Sigma; ::_thesis: ( A c= B implies P . (B \ A) = (P . B) - (P . A) )
assume A1: A c= B ; ::_thesis: P . (B \ A) = (P . B) - (P . A)
 A misses B \ A by XBOOLE_1:79;
then (P . A) + (P . (B \ A)) = P . (A \/ (B \ A)) by Def8
.= P . B by A1, XBOOLE_1:45 ;
hence  P . (B \ A) = (P . B) - (P . A) ; ::_thesis: verum
end;

theorem Th34: :: PROB_1:34
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . A <= P . B
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . A <= P . B
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . A <= P . B
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A c= B holds
P . A <= P . B
let P be Probability of Sigma; ::_thesis: ( A c= B implies P . A <= P . B )
assume  A c= B ; ::_thesis: P . A <= P . B
then  P . (B \ A) = (P . B) - (P . A) by Th33;
then  0 <= (P . B) - (P . A) by Def8;
then  0 + (P . A) <= P . B by XREAL_1:19;
hence  P . A <= P . B ; ::_thesis: verum
end;

theorem :: PROB_1:35
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . A <= 1
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . A <= 1
let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma
for P being Probability of Sigma holds P . A <= 1
let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . A <= 1
let P be Probability of Sigma; ::_thesis: P . A <= 1
 P . ([#] Sigma) = 1 by Def8;
hence  P . A <= 1 by Th34; ::_thesis: verum
end;

theorem Th36: :: PROB_1:36
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))
let P be Probability of Sigma; ::_thesis: P . (A \/ B) = (P . A) + (P . (B \ A))
A1: A misses B \ A by XBOOLE_1:79;
P . (A \/ B) = P . (A \/ (B \ A)) by XBOOLE_1:39
.= (P . A) + (P . (B \ A)) by A1, Def8 ;
hence  P . (A \/ B) = (P . A) + (P . (B \ A)) ; ::_thesis: verum
end;

theorem Th37: :: PROB_1:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
let P be Probability of Sigma; ::_thesis: P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
thus P . (A \/ B) = (P . A) + (P . (B \ A)) by Th36
.= (P . A) + (P . (B \ (A /\ B))) by XBOOLE_1:47 ; ::_thesis: verum
end;

theorem Th38: :: PROB_1:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
let P be Probability of Sigma; ::_thesis: P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
P . (A \/ B) = (P . A) + (P . (B \ (A /\ B))) by Th37
.= (P . A) + ((P . B) - (P . (A /\ B))) by Th33, XBOOLE_1:17 ;
hence  P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) ; ::_thesis: verum
end;

theorem :: PROB_1:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
let P be Probability of Sigma; ::_thesis: P . (A \/ B) <= (P . A) + (P . B)
 ( 0 <= P . (A /\ B) & P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) ) by Def8, Th38;
hence  P . (A \/ B) <= (P . A) + (P . B) by XREAL_1:43; ::_thesis: verum
end;


theorem :: PROB_1:40
for X being set holds bool X is SigmaField of X ;

definition
let Omega be non empty set ;
let X be Subset-Family of Omega;
func sigma X ->  SigmaField of Omega means :: PROB_1:def 9
( X c= it & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
it c= Z ) );
existence
 ex b1 being SigmaField of Omega st
( X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b1 c= Z ) )
proof
set V =  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ;
set Y = meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ;
A1: now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_
X_c=_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies X c= Z )
assume  Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: X c= Z
then  ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;
hence  X c= Z ; ::_thesis: verum
end;
A2: bool Omega in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ;
A3: for E being Subset of Omega st E in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  holds
E ` in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }
proof
let E be Subset of Omega; ::_thesis: ( E in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies E ` in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  )
assume A4: E in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: E ` in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_
E_`_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies E ` in Z )
assume  Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: E ` in Z
then  ( E in Z & ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ) by A4, SETFAM_1:def_1;
hence  E ` in Z by Def1; ::_thesis: verum
end;
hence  E ` in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  by A2, SETFAM_1:def_1; ::_thesis: verum
end;
A5: for BSeq being SetSequence of Omega st rng BSeq c= meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  holds
Intersection BSeq in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }
proof
let BSeq be SetSequence of Omega; ::_thesis: ( rng BSeq c= meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies Intersection BSeq in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  )
assume A6: rng BSeq c= meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: Intersection BSeq in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_
Intersection_BSeq_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies Intersection BSeq in Z )
assume A7: Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: Intersection BSeq in Z
now__::_thesis:_for_n_being_Nat_holds_BSeq_._n_in_Z
let n be Nat; ::_thesis: BSeq . n in Z
 BSeq . n in rng BSeq by NAT_1:51;
hence  BSeq . n in Z by A6, A7, SETFAM_1:def_1; ::_thesis: verum
end;
then A8: rng BSeq c= Z by NAT_1:52;
 ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) by A7;
hence  Intersection BSeq in Z by A8, Def6; ::_thesis: verum
end;
hence  Intersection BSeq in meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  by A2, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_Omega_:_(_X_c=_S_&_S_is_SigmaField_of_Omega_)__}__holds_
{}_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  implies {} in Z )
assume  Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  ; ::_thesis: {} in Z
then  ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;
hence  {} in Z by Th4; ::_thesis: verum
end;
then reconsider Y = meet  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  as SigmaField of Omega by A2, A5, A3, Def1, Def6, SETFAM_1:3, SETFAM_1:def_1;
take  Y ; ::_thesis: ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) )
 for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z
proof
let Z be set ; ::_thesis: ( X c= Z & Z is SigmaField of Omega implies Y c= Z )
assume that
A9: X c= Z and
A10: Z is SigmaField of Omega ; ::_thesis: Y c= Z
reconsider Z = Z as Subset-Family of Omega by A10;
 Z in  {  S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega )  }  by A9, A10;
hence  Y c= Z by SETFAM_1:3; ::_thesis: verum
end;
hence  ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SigmaField of Omega st X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b1 c= Z ) & X c= b2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b2 c= Z ) holds
b1 = b2
proof
let R1, R2 be SigmaField of Omega; ::_thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
R2 c= Z ) implies R1 = R2 )
assume  ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
R2 c= Z ) ) ; ::_thesis: R1 = R2
then  ( R1 c= R2 & R2 c= R1 ) ;
hence  R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem  defines sigma PROB_1:def_9_:_
 for Omega being non empty set
for X being Subset-Family of Omega
for b3 being SigmaField of Omega holds
( b3 = sigma X iff ( X c= b3 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b3 c= Z ) ) );

definition
let r be ext-real number ;
func halfline r ->  Subset of REAL equals :: PROB_1:def 10
].-infty,r.[;
coherence
 ].-infty,r.[ is Subset of REAL
proof
 ].-infty,r.[ c= REAL
proof
let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in ].-infty,r.[ or x in REAL )
assume  x in ].-infty,r.[ ; ::_thesis: x in REAL
then  ( -infty < x & x < r ) by XXREAL_1:4;
hence  x in REAL by XXREAL_0:48; ::_thesis: verum
end;
hence  ].-infty,r.[ is Subset of REAL ; ::_thesis: verum
end;
end;

:: deftheorem  defines halfline PROB_1:def_10_:_
 for r being ext-real number holds halfline r = ].-infty,r.[;

definition
func Family_of_halflines  ->  Subset-Family of REAL equals :: PROB_1:def 11
 {  (halfline r) where r is Element of REAL : verum  }  ;
coherence
  {  (halfline r) where r is Element of REAL : verum  }  is Subset-Family of REAL
proof
  {  (halfline r) where r is Element of REAL : verum  }  c= bool REAL
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in  {  (halfline r) where r is Element of REAL : verum  }  or p in bool REAL )
assume  p in  {  (halfline r) where r is Element of REAL : verum  }  ; ::_thesis: p in bool REAL
then  ex r being Element of REAL st p = halfline r ;
hence  p in bool REAL ; ::_thesis: verum
end;
hence   {  (halfline r) where r is Element of REAL : verum  }  is Subset-Family of REAL ; ::_thesis: verum
end;
end;

:: deftheorem  defines Family_of_halflines PROB_1:def_11_:_
 Family_of_halflines =  {  (halfline r) where r is Element of REAL : verum  }  ;

definition
func Borel_Sets  ->  SigmaField of REAL equals :: PROB_1:def 12
 sigma Family_of_halflines;
correctness
coherence
sigma Family_of_halflines is SigmaField of REAL;
;
end;

:: deftheorem  defines Borel_Sets PROB_1:def_12_:_
 Borel_Sets = sigma Family_of_halflines;

theorem :: PROB_1:41
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

definition
let X, Y be set ;
let A be Subset-Family of X;
let F be Function of Y,(bool A);
let x be set ;
:: original: .
redefine funcF . x ->  Subset-Family of X;
coherence
 F . x is Subset-Family of X
proof
percases ( x in dom F or not x in dom F ) ;
supposeA1: x in dom F ; ::_thesis: F . x is Subset-Family of X
A2: rng F c= bool A by RELAT_1:def_19;
A3: bool A c= bool (bool X) by ZFMISC_1:67;
 F . x in rng F by A1, FUNCT_1:def_3;
then  F . x in bool A by A2;
hence  F . x is Subset-Family of X by A3; ::_thesis: verum
end;
suppose not x in dom F ; ::_thesis: F . x is Subset-Family of X
then  F . x = {} by FUNCT_1:def_2;
hence  F . x is Subset-Family of X by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
end;