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 } ;

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 }

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;

then A4: Family_of_halflines c= { 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;

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

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;

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