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

for f being Function of Omega,REAL st f is Real-Valued-Random-Variable of Sigma holds

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL st f is Real-Valued-Random-Variable of Sigma holds

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

let f be Function of Omega,REAL; :: thesis: ( f is Real-Valued-Random-Variable of Sigma implies { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets )

assume A1: f is Real-Valued-Random-Variable of Sigma ; :: thesis: { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

set B = { x where x is Element of Borel_Sets : f " x is Element of Sigma } ;

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } is SigmaField of REAL by Th5, A1;

then A5: Borel_Sets c= { x where x is Element of Borel_Sets : f " x is Element of Sigma } by A4, PROB_1:def 9;

hence { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets by A5; :: thesis: verum

for f being Function of Omega,REAL st f is Real-Valued-Random-Variable of Sigma holds

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL st f is Real-Valued-Random-Variable of Sigma holds

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

let f be Function of Omega,REAL; :: thesis: ( f is Real-Valued-Random-Variable of Sigma implies { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets )

assume A1: f is Real-Valued-Random-Variable of Sigma ; :: thesis: { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets

set B = { x where x is Element of Borel_Sets : f " x is Element of Sigma } ;

now :: thesis: for z being object st z in Family_of_halflines holds

z in { x where x is Element of Borel_Sets : f " x is Element of Sigma }

then A4:
Family_of_halflines c= { x where x is Element of Borel_Sets : f " x is Element of Sigma }
;z in { x where x is Element of Borel_Sets : f " x is Element of Sigma }

let z be object ; :: thesis: ( z in Family_of_halflines implies z in { x where x is Element of Borel_Sets : f " x is Element of Sigma } )

assume A2: z in Family_of_halflines ; :: thesis: z in { x where x is Element of Borel_Sets : f " x is Element of Sigma }

Family_of_halflines c= sigma Family_of_halflines by PROB_1:def 9;

then reconsider y = z as Element of Borel_Sets by A2;

consider r being Element of REAL such that

A3: y = halfline r by A2;

f " y is Element of Sigma by A1, Th4, A3;

hence z in { x where x is Element of Borel_Sets : f " x is Element of Sigma } ; :: thesis: verum

end;assume A2: z in Family_of_halflines ; :: thesis: z in { x where x is Element of Borel_Sets : f " x is Element of Sigma }

Family_of_halflines c= sigma Family_of_halflines by PROB_1:def 9;

then reconsider y = z as Element of Borel_Sets by A2;

consider r being Element of REAL such that

A3: y = halfline r by A2;

f " y is Element of Sigma by A1, Th4, A3;

hence z in { x where x is Element of Borel_Sets : f " x is Element of Sigma } ; :: thesis: verum

{ x where x is Element of Borel_Sets : f " x is Element of Sigma } is SigmaField of REAL by Th5, A1;

then A5: Borel_Sets c= { x where x is Element of Borel_Sets : f " x is Element of Sigma } by A4, PROB_1:def 9;

now :: thesis: for x being object st x in { x where x is Element of Borel_Sets : f " x is Element of Sigma } holds

x in Borel_Sets

then
{ x where x is Element of Borel_Sets : f " x is Element of Sigma } c= Borel_Sets
;x in Borel_Sets

let x be object ; :: thesis: ( x in { x where x is Element of Borel_Sets : f " x is Element of Sigma } implies x in Borel_Sets )

assume x in { x where x is Element of Borel_Sets : f " x is Element of Sigma } ; :: thesis: x in Borel_Sets

then ex z being Element of Borel_Sets st

( z = x & f " z is Element of Sigma ) ;

hence x in Borel_Sets ; :: thesis: verum

end;assume x in { x where x is Element of Borel_Sets : f " x is Element of Sigma } ; :: thesis: x in Borel_Sets

then ex z being Element of Borel_Sets st

( z = x & f " z is Element of Sigma ) ;

hence x in Borel_Sets ; :: thesis: verum

hence { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets by A5; :: thesis: verum