let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let X be Function of Omega,REAL; :: thesis:
assume A0: X is_random_variable_on Sigma, Borel_Sets ; :: thesis:
Fin0: for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )

let k be real number ; :: thesis:
CJ1: for q being set holds
( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )

let q be set ; :: thesis:

now

assume ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ; :: thesis:
then consider w being Element of Omega such that
T0: ( q = w & X . w in [.k,+infty.] ) ;
X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by T0, XXREAL_1:def 1;
then ex z being Element of ExtREAL st
( X . w = z & k <= z & z <= +infty ) ;
hence ex w being Element of Omega st
( q = w & X . w >= k ) by T0; :: thesis:

end;

hence ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ) by XXREAL_1:219; :: thesis:

end;

GG: for x being set holds
( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w >= k ) ) ;
then H00: ( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w in [.k,+infty.] ) ) by CJ1;
( x in { w where w is Element of Omega : X . w in [.k,+infty.] } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )

proof

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis:
then consider w being Element of Omega such that
EJ0: ( w = x & X . w in [.k,+infty.] ) ;
X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by EJ0, XXREAL_1:def 1;
then consider a being Element of ExtREAL such that
EJ1: ( X . w = a & k <= a & a <= +infty ) ;
EJ2: ( X . w = a & k <= a & a < +infty ) by EJ1, XXREAL_0:9;
{ z where z is Element of ExtREAL : ( k <= z & z < +infty ) } = [.k,+infty.[ by XXREAL_1:def 2;
then X . w in [.k,+infty.[ by EJ2;
hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by EJ0; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis:
then consider w being Element of Omega such that
II0: ( w = x & X . w in [.k,+infty.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by II0, XXREAL_1:def 2;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & k <= u & u < +infty ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u <= +infty ) } ) ;
then ( w = x & X . w in [.k,+infty.] ) by XXREAL_1:def 1;
hence x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis:

end;

hence ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ) by H00; :: thesis:

end;

k in REAL by XREAL_0:def 1;
then QQ: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;
UUU: { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }

proof

{ w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }

proof

for x being set holds
( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis:
then ex w being Element of Omega st
( w = x & X . w in [.k,+infty.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis:
then consider w being Element of Omega such that
K0: ( w = x & X . w is Element of [.k,+infty.[ ) ;
thus x in { w where w is Element of Omega : X . w in [.k,+infty.[ } by K0, QQ; :: thesis:

end;

hence { w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by TARSKI:1; :: thesis:

end;

hence { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by GG, TARSKI:1; :: thesis:

end;

ff: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by BJ1;
CJ4: for q being set holds
( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )

proof

let q be set ; :: thesis:

now

assume ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ; :: thesis:
then consider w being Element of Omega such that
T0: ( q = w & X . w in [.-infty,k.[ ) ;
X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by T0, XXREAL_1:def 2;
then ex z being Element of ExtREAL st
( X . w = z & -infty <= z & z < k ) ;
hence ex w being Element of Omega st
( q = w & X . w < k ) by T0; :: thesis:

end;

hence ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ) by XXREAL_1:221; :: thesis:

end;

for x being set holds
( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w < k ) ) ;
then H00: ( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w in [.-infty,k.[ ) ) by CJ4;
( x in { w where w is Element of Omega : X . w in [.-infty,k.[ } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )

proof

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
EJ0: ( w = x & X . w in [.-infty,k.[ ) ;
X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by EJ0, XXREAL_1:def 2;
then consider a being Element of ExtREAL such that
EJ1: ( X . w = a & -infty <= a & a < k ) ;
EJ2: ( X . w = a & -infty < a & a < k ) by EJ1, XXREAL_0:12;
{ z where z is Element of ExtREAL : ( -infty < z & z < k ) } = ].-infty,k.[ by XXREAL_1:def 4;
then X . w in ].-infty,k.[ by EJ2;
hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by EJ0; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
II0: ( w = x & X . w in ].-infty,k.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by II0, XXREAL_1:def 4;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & -infty < u & u < k ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( -infty <= u & u < k ) } ) ;
then ( w = x & X . w in [.-infty,k.[ ) by XXREAL_1:def 2;
hence x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis:

end;

hence ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ) by H00; :: thesis:

end;

then GGG: { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w in ].-infty,k.[ } by TARSKI:1;
{ w where w is Element of Omega : X . w < k } is Element of Sigma

proof

FJ30: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by BJ1;
k in REAL by XREAL_0:def 1;
then QQ: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;
for x being set holds
( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis:
then ex w being Element of Omega st
( w = x & X . w in ].-infty,k.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
K0: ( w = x & X . w is Element of ].-infty,k.[ ) ;
thus x in { w where w is Element of Omega : X . w in ].-infty,k.[ } by K0, QQ; :: thesis:

end;

then { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } by GGG, TARSKI:1;
hence { w where w is Element of Omega : X . w < k } is Element of Sigma by FJ30, A0, Def8; :: thesis:

end;

hence ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) by ff, A0, Def8, UUU; :: thesis:

end;

Fin1: for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma

proof

let k1, k2 be real number ; :: thesis:
assume A1: k1 < k2 ; :: thesis:
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma

proof

for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } ; :: thesis:
then consider w being Element of Omega such that
GJ0: ( x = w & k1 <= X . w & X . w < k2 ) ;
consider a being Element of ExtREAL such that
GJ02: a = R_EAL (X . w) ;
a = X . w by GJ02, MEASURE6:def 1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by GJ0;
then X . w is Element of [.k1,k2.[ by XXREAL_1:def 2;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ } by GJ0; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } ; :: thesis:
then consider w being Element of Omega such that
GJ0: ( x = w & X . w is Element of [.k1,k2.[ ) ;
GJ2: not [.k1,k2.[ is empty by A1, XXREAL_1:31;
X . w in [.k1,k2.[ by GJ0, GJ2;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a < k2 ) } by XXREAL_1:def 2;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a < k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } by GJ0; :: thesis:

end;

then GGG: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } by TARSKI:1;
( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by BJ2;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A0, Def8, GGG; :: thesis:

end;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ; :: thesis:

end;

Fin2: for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma

proof

let k1, k2 be real number ; :: thesis:
assume AA0: k1 <= k2 ; :: thesis:
for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } ; :: thesis:
then consider w being Element of Omega such that
GJ0: ( x = w & k1 <= X . w & X . w <= k2 ) ;
consider a being Element of ExtREAL such that
GJ02: a = R_EAL (X . w) ;
a = X . w by GJ02, MEASURE6:def 1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by GJ0;
then X . w is Element of [.k1,k2.] by XXREAL_1:def 1;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] } by GJ0; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } ; :: thesis:
then consider w being Element of Omega such that
GJ0: ( x = w & X . w is Element of [.k1,k2.] ) ;
GJ2: not [.k1,k2.] is empty by AA0, XXREAL_1:30;
X . w in [.k1,k2.] by GJ0, GJ2;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a <= k2 ) } by XXREAL_1:def 1;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a <= k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } by GJ0; :: thesis:

end;

then GGG: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.] } by TARSKI:1;
( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th3, BJ2;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A0, Def8, GGG; :: thesis:

end;

Fin3: for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )

proof

let x be set ; :: thesis:
( x in less_dom (X,r) iff ( x in dom X & X . x < r ) ) by MESFUNC1:def 11;
then ( x in less_dom (X,r) iff ( x in Omega & X . x < r ) ) by FUNCT_2:def 1;
then ( x in less_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q < r ) ) ;
hence ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } ) ; :: thesis:

end;

hence less_dom (X,r) = { w where w is Element of Omega : X . w < r } by TARSKI:1; :: thesis:

end;

Fin4: for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )

proof

let x be set ; :: thesis:
( x in great_eq_dom (X,r) iff ( x in dom X & X . x >= r ) ) by MESFUNC1:def 14;
then ( x in great_eq_dom (X,r) iff ( x in Omega & X . x >= r ) ) by FUNCT_2:def 1;
then ( x in great_eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q >= r ) ) ;
hence ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } ) ; :: thesis:

end;

hence great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } by TARSKI:1; :: thesis:

end;

Fin5: for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )

proof

let x be set ; :: thesis:
( x in eq_dom (X,r) iff ( x in dom X & X . x = r ) ) by MESFUNC1:def 15;
then ( x in eq_dom (X,r) iff ( x in Omega & X . x = r ) ) by FUNCT_2:def 1;
then ( x in eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q = r ) ) ;
hence ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis:

end;

hence eq_dom (X,r) = { w where w is Element of Omega : X . w = r } by TARSKI:1; :: thesis:

end;

for r being real number holds eq_dom (X,r) is Element of Sigma

proof

let r be real number ; :: thesis:
for x being set holds
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & r <= X . q & X . q <= r ) ) ;
then ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & X . q = r ) ) by XXREAL_0:1;
hence ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis:

end;

then { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } = { w where w is Element of Omega : X . w = r } by TARSKI:1;
then { w where w is Element of Omega : X . w = r } is Element of Sigma by Fin2;
hence eq_dom (X,r) is Element of Sigma by Fin5; :: thesis:

end;

hence ( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) ) by Fin0, Fin1, Fin2, Fin3, Fin4, Fin5; :: thesis: