let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

let Sigma be SigmaField of Omega; :: thesis: for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

let X be Function of Omega,REAL; :: thesis: ( X is Sigma, Borel_Sets -random_variable-like implies ( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) )

assume A1: X is Sigma, Borel_Sets -random_variable-like ; :: thesis: ( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

A2: for k being Real 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 )

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

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

( { 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) by A2, A28, A36, A44, A45, A46; :: thesis: verum

for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

let Sigma be SigmaField of Omega; :: thesis: for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

let X be Function of Omega,REAL; :: thesis: ( X is Sigma, Borel_Sets -random_variable-like implies ( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) )

assume A1: X is Sigma, Borel_Sets -random_variable-like ; :: thesis: ( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

A2: for k being Real 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 )

proof

A28:
for k1, k2 being Real st k1 < k2 holds
let k be Real; :: thesis: ( { 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 )

A3: 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.] ) )

( 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.[ } )

then A11: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;

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

A15: { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } = X " [.k,+infty.[ by Lm1, A11;

A16: 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.[ ) )

( 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.[ } )

{ w where w is Element of Omega : X . w < k } is Element of Sigma

end;A3: 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.] ) )

proof

A5:
for x being object holds
let q be set ; :: thesis: ( 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.] ) )

( 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: verum

end;( q = w & X . w >= k ) iff ex w being Element of Omega st

( q = w & X . w in [.k,+infty.] ) )

now :: thesis: ( ex w being Element of Omega st

( q = w & X . w in [.k,+infty.] ) implies ex w being Element of Omega st

( q = w & X . w >= k ) )

hence
( ex w being Element of Omega st ( q = w & X . w in [.k,+infty.] ) implies ex w being Element of Omega st

( q = w & X . w >= k ) )

assume
ex w being Element of Omega st

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

( q = w & X . w >= k )

then consider w being Element of Omega such that

A4: ( q = w & X . w in [.k,+infty.] ) ;

X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by A4, 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 A4; :: thesis: verum

end;( q = w & X . w in [.k,+infty.] ) ; :: thesis: ex w being Element of Omega st

( q = w & X . w >= k )

then consider w being Element of Omega such that

A4: ( q = w & X . w in [.k,+infty.] ) ;

X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by A4, 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 A4; :: thesis: verum

( 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: verum

( 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

k in REAL
by XREAL_0:def 1;
let x be object ; :: thesis: ( 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.[ } )

( 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 A6: ( 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 A3;

( 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.[ } )

end;( 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 A6: ( 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 A3;

( 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

then consider w being Element of Omega such that

A10: ( w = x & X . w in [.k,+infty.[ ) ;

( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by A10, 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: verum

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 A6; :: thesis: verumhereby :: thesis: ( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.] } )

assume
x in { w where w is Element of Omega : X . w in [.k,+infty.[ }
; :: thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.] } assume
x in { w where w is Element of Omega : X . w in [.k,+infty.] }
; :: thesis: x in { g where g is Element of Omega : X . g in [.k,+infty.[ }

then consider w being Element of Omega such that

A7: ( w = x & X . w in [.k,+infty.] ) ;

X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by A7, XXREAL_1:def 1;

then consider a being Element of ExtREAL such that

A8: ( X . w = a & k <= a & a <= +infty ) ;

A9: ( X . w = a & k <= a & a < +infty ) by A8, 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 A9;

hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by A7; :: thesis: verum

end;then consider w being Element of Omega such that

A7: ( w = x & X . w in [.k,+infty.] ) ;

X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by A7, XXREAL_1:def 1;

then consider a being Element of ExtREAL such that

A8: ( X . w = a & k <= a & a <= +infty ) ;

A9: ( X . w = a & k <= a & a < +infty ) by A8, 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 A9;

hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by A7; :: thesis: verum

then consider w being Element of Omega such that

A10: ( w = x & X . w in [.k,+infty.[ ) ;

( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by A10, 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: verum

then A11: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;

A12: { 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

A14:
( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
by Th3;
{ 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.[ }

end;proof

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 A5, TARSKI:2; :: thesis: verum
for x being object 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.[ } )

end;( 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

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:2; :: thesis: verum
let x be object ; :: thesis: ( 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.[ } )

then consider w being Element of Omega such that

A13: ( 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 A13, A11; :: thesis: verum

end;hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )

assume
x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
; :: thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.[ } assume
x in { w where w is Element of Omega : X . w in [.k,+infty.[ }
; :: thesis: x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }

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: verum

end;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: verum

then consider w being Element of Omega such that

A13: ( 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 A13, A11; :: thesis: verum

A15: { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } = X " [.k,+infty.[ by Lm1, A11;

A16: 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

for x being object holds
let q be set ; :: thesis: ( 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.[ ) )

( 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: verum

end;( q = w & X . w < k ) iff ex w being Element of Omega st

( q = w & X . w in [.-infty,k.[ ) )

now :: thesis: ( ex w being Element of Omega st

( q = w & X . w in [.-infty,k.[ ) implies ex w being Element of Omega st

( q = w & X . w < k ) )

hence
( ex w being Element of Omega st ( q = w & X . w in [.-infty,k.[ ) implies ex w being Element of Omega st

( q = w & X . w < k ) )

assume
ex w being Element of Omega st

( q = w & X . w in [.-infty,k.[ ) ; :: thesis: ex w being Element of Omega st

( q = w & X . w < k )

then consider w being Element of Omega such that

A17: ( q = w & X . w in [.-infty,k.[ ) ;

X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by A17, 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 A17; :: thesis: verum

end;( q = w & X . w in [.-infty,k.[ ) ; :: thesis: ex w being Element of Omega st

( q = w & X . w < k )

then consider w being Element of Omega such that

A17: ( q = w & X . w in [.-infty,k.[ ) ;

X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by A17, 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 A17; :: thesis: verum

( 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: verum

( 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

then A23:
{ w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w in ].-infty,k.[ }
by TARSKI:2;
let x be object ; :: thesis: ( 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.[ } )

( 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 A18: ( 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 A16;

( 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.[ } )

end;( 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 A18: ( 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 A16;

( 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

then consider w being Element of Omega such that

A22: ( w = x & X . w in ].-infty,k.[ ) ;

( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by A22, 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: verum

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 A18; :: thesis: verumhereby :: thesis: ( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in [.-infty,k.[ } )

assume
x in { w where w is Element of Omega : X . w in ].-infty,k.[ }
; :: thesis: x in { w where w is Element of Omega : X . w in [.-infty,k.[ } assume
x in { w where w is Element of Omega : X . w in [.-infty,k.[ }
; :: thesis: x in { g where g is Element of Omega : X . g in ].-infty,k.[ }

then consider w being Element of Omega such that

A19: ( w = x & X . w in [.-infty,k.[ ) ;

X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by A19, XXREAL_1:def 2;

then consider a being Element of ExtREAL such that

A20: ( X . w = a & -infty <= a & a < k ) ;

A21: ( X . w = a & -infty < a & a < k ) by A20, 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 A21;

hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by A19; :: thesis: verum

end;then consider w being Element of Omega such that

A19: ( w = x & X . w in [.-infty,k.[ ) ;

X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by A19, XXREAL_1:def 2;

then consider a being Element of ExtREAL such that

A20: ( X . w = a & -infty <= a & a < k ) ;

A21: ( X . w = a & -infty < a & a < k ) by A20, 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 A21;

hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by A19; :: thesis: verum

then consider w being Element of Omega such that

A22: ( w = x & X . w in ].-infty,k.[ ) ;

( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by A22, 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: verum

{ w where w is Element of Omega : X . w < k } is Element of Sigma

proof

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 A14, A1, A12, A15; :: thesis: verum
A24:
( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
by Th3;

k in REAL by XREAL_0:def 1;

then A25: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;

then A26: { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } = X " ].-infty,k.[ by Lm1;

for x being object 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.[ } )

.= X " ].-infty,k.[ by A26 ;

hence { w where w is Element of Omega : X . w < k } is Element of Sigma by A24, A1; :: thesis: verum

end;k in REAL by XREAL_0:def 1;

then A25: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;

then A26: { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } = X " ].-infty,k.[ by Lm1;

for x being object 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

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 A23, TARSKI:2
let x be object ; :: thesis: ( 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.[ } )

then consider w being Element of Omega such that

A27: ( 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 A27, A25; :: thesis: verum

end;hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )

assume
x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ }
; :: thesis: x in { w where w is Element of Omega : X . w in ].-infty,k.[ } assume
x in { w where w is Element of Omega : X . w in ].-infty,k.[ }
; :: thesis: x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ }

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: verum

end;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: verum

then consider w being Element of Omega such that

A27: ( 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 A27, A25; :: thesis: verum

.= X " ].-infty,k.[ by A26 ;

hence { w where w is Element of Omega : X . w < k } is Element of Sigma by A24, A1; :: thesis: verum

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

proof

A36:
for k1, k2 being Real st k1 <= k2 holds
let k1, k2 be Real; :: thesis: ( k1 < k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma )

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

then A30: not [.k1,k2.[ is empty by XXREAL_1:31;

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

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

then A30: not [.k1,k2.[ is empty by XXREAL_1:31;

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

proof

hence
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
; :: thesis: verum
for x being object 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.[ } )

A35: ( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by Th4;

{ w where w is Element of Omega : X . w is Element of [.k1,k2.[ } = X " [.k1,k2.[ by Lm1, A30;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A1, A34, A35; :: thesis: verum

end;( 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

then A34:
{ 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:2;
let x be object ; :: thesis: ( 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.[ } )

then consider w being Element of Omega such that

A32: ( x = w & X . w is Element of [.k1,k2.[ ) ;

A33: not [.k1,k2.[ is empty by A29, XXREAL_1:31;

X . w in [.k1,k2.[ by A32, A33;

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 A32; :: thesis: verum

end;hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } )

assume
x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ }
; :: thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } assume
x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) }
; :: thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ }

then consider w being Element of Omega such that

A31: ( x = w & k1 <= X . w & X . w < k2 ) ;

reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;

a = X . w ;

then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by A31;

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 A31; :: thesis: verum

end;then consider w being Element of Omega such that

A31: ( x = w & k1 <= X . w & X . w < k2 ) ;

reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;

a = X . w ;

then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by A31;

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 A31; :: thesis: verum

then consider w being Element of Omega such that

A32: ( x = w & X . w is Element of [.k1,k2.[ ) ;

A33: not [.k1,k2.[ is empty by A29, XXREAL_1:31;

X . w in [.k1,k2.[ by A32, A33;

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 A32; :: thesis: verum

A35: ( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by Th4;

{ w where w is Element of Omega : X . w is Element of [.k1,k2.[ } = X " [.k1,k2.[ by Lm1, A30;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A1, A34, A35; :: thesis: verum

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

proof

A44:
for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r }
let k1, k2 be Real; :: thesis: ( k1 <= k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma )

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

then A38: not [.k1,k2.] is empty by XXREAL_1:30;

for x being object 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.] } )

A43: ( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th8, Th4;

{ w where w is Element of Omega : X . w is Element of [.k1,k2.] } = X " [.k1,k2.] by Lm1, A38;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A1, A42, A43; :: thesis: verum

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

then A38: not [.k1,k2.] is empty by XXREAL_1:30;

for x being object 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

then A42:
{ 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:2;
let x be object ; :: thesis: ( 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.] } )

then consider w being Element of Omega such that

A40: ( x = w & X . w is Element of [.k1,k2.] ) ;

A41: not [.k1,k2.] is empty by A37, XXREAL_1:30;

X . w in [.k1,k2.] by A40, A41;

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 A40; :: thesis: verum

end;hereby :: thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } )

assume
x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] }
; :: thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } assume
x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) }
; :: thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] }

then consider w being Element of Omega such that

A39: ( x = w & k1 <= X . w & X . w <= k2 ) ;

reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;

a = X . w ;

then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by A39;

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 A39; :: thesis: verum

end;then consider w being Element of Omega such that

A39: ( x = w & k1 <= X . w & X . w <= k2 ) ;

reconsider a = X . w as Element of ExtREAL by XXREAL_0:def 1;

a = X . w ;

then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by A39;

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 A39; :: thesis: verum

then consider w being Element of Omega such that

A40: ( x = w & X . w is Element of [.k1,k2.] ) ;

A41: not [.k1,k2.] is empty by A37, XXREAL_1:30;

X . w in [.k1,k2.] by A40, A41;

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 A40; :: thesis: verum

A43: ( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th8, Th4;

{ w where w is Element of Omega : X . w is Element of [.k1,k2.] } = X " [.k1,k2.] by Lm1, A38;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A1, A42, A43; :: thesis: verum

proof

A45:
for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
let r be Real; :: thesis: less_dom (X,r) = { w where w is Element of Omega : X . w < r }

for x being object holds

( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )

end;for x being object holds

( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )

proof

hence
less_dom (X,r) = { w where w is Element of Omega : X . w < r }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )

reconsider xx = x as set by TARSKI:1;

( x in less_dom (X,r) iff ( x in dom X & X . xx < r ) ) by MESFUNC1:def 11;

then ( x in less_dom (X,r) iff ( x in Omega & X . xx < 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: verum

end;reconsider xx = x as set by TARSKI:1;

( x in less_dom (X,r) iff ( x in dom X & X . xx < r ) ) by MESFUNC1:def 11;

then ( x in less_dom (X,r) iff ( x in Omega & X . xx < 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: verum

proof

A46:
for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
let r be Real; :: thesis: great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }

for x being object holds

( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )

end;for x being object holds

( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )

proof

hence
great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )

reconsider xx = x as set by TARSKI:1;

( x in great_eq_dom (X,r) iff ( x in dom X & X . xx >= r ) ) by MESFUNC1:def 14;

then ( x in great_eq_dom (X,r) iff ( x in Omega & X . xx >= 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: verum

end;reconsider xx = x as set by TARSKI:1;

( x in great_eq_dom (X,r) iff ( x in dom X & X . xx >= r ) ) by MESFUNC1:def 14;

then ( x in great_eq_dom (X,r) iff ( x in Omega & X . xx >= 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: verum

proof

for r being Real holds eq_dom (X,r) is Element of Sigma
let r be Real; :: thesis: eq_dom (X,r) = { w where w is Element of Omega : X . w = r }

for x being object holds

( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )

end;for x being object holds

( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )

proof

hence
eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )

( 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: verum

end;( 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: verum

proof

hence
( ( for k being Real holds
let r be Real; :: thesis: eq_dom (X,r) is Element of Sigma

for x being object 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 } )

then { w where w is Element of Omega : X . w = r } is Element of Sigma by A36;

hence eq_dom (X,r) is Element of Sigma by A46; :: thesis: verum

end;for x being object 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

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:2;
let x be object ; :: thesis: ( 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 } )

( 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: verum

end;( 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: verum

then { w where w is Element of Omega : X . w = r } is Element of Sigma by A36;

hence eq_dom (X,r) is Element of Sigma by A46; :: thesis: verum

( { 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) ) by A2, A28, A36, A44, A45, A46; :: thesis: verum