A1: sigma Family_of_halflines2 c= sigma Family_of_halflines

proof

Family_of_halflines2 c= sigma Family_of_halflines

proof

for x being object st x in Family_of_halflines2 holds
x in sigma Family_of_halflines

proof

let x be object ; :: thesis: ( x in Family_of_halflines2 implies x in sigma Family_of_halflines )
assume x in Family_of_halflines2 ; :: thesis: x in sigma Family_of_halflines
then consider r being Element of REAL such that
B1: x = right_closed_halfline r ;
x is Element of Borel_Sets by FINANCE1:3, B1;
hence x in sigma Family_of_halflines ; :: thesis: verum

end;

hence Family_of_halflines2 c= sigma Family_of_halflines ; :: thesis: verum

end;

hence sigma Family_of_halflines2 c= sigma Family_of_halflines by PROB_1:def 9; :: thesis: verum

end;

sigma Family_of_halflines c= sigma Family_of_halflines2

proof

Family_of_halflines c= sigma Family_of_halflines2

proof

for x being object st x in Family_of_halflines holds
x in sigma Family_of_halflines2

proof

let x be object ; :: thesis: ( x in Family_of_halflines implies x in sigma Family_of_halflines2 )
assume x in Family_of_halflines ; :: thesis: x in sigma Family_of_halflines2
then consider r being Element of REAL such that
B1: x = halfline r ;
right_closed_halfline r is Event of sigma Family_of_halflines2

proof

set L = right_closed_halfline r;
A3: ( right_closed_halfline r in Family_of_halflines2 & right_closed_halfline r = [.r,+infty.[ ) ;
Family_of_halflines2 c= sigma Family_of_halflines2 by PROB_1:def 9;
hence right_closed_halfline r is Event of sigma Family_of_halflines2 by A3; :: thesis: verum

end;

then (halfline r) ` is Event of sigma Family_of_halflines2 by FINANCE1:2;
then ((halfline r) `) ` is Event of sigma Family_of_halflines2 by PROB_1:15;
hence x in sigma Family_of_halflines2 by B1; :: thesis: verum

end;

hence Family_of_halflines c= sigma Family_of_halflines2 ; :: thesis: verum

end;

hence sigma Family_of_halflines c= sigma Family_of_halflines2 by PROB_1:def 9; :: thesis: verum

end;

hence Borel_Sets = sigma Family_of_halflines2 by A1; :: thesis: verum