let a, b be real number ; :: thesis: Intersection (half_open_sets (a,b)) is Element of Borel_Sets
for n being Element of NAT holds (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets

proof

let n be Element of NAT ; :: thesis: (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets
((half_open_sets (a,b)) . n) ` is Element of Borel_Sets

proof

(half_open_sets (a,b)) . n is Element of Borel_Sets

proof

per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;

suppose CJ00: n = 0 ; :: thesis: (half_open_sets (a,b)) . n is Element of Borel_Sets

(half_open_sets (a,b)) . 0 = halfline_fin (a,(b + 1)) by Def3;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by CJ00, BJ2; :: thesis: verum

end;

suppose ex k being Nat st n = k + 1 ; :: thesis: (half_open_sets (a,b)) . n is Element of Borel_Sets

then consider k being Nat such that
CJ00: n = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(half_open_sets (a,b)) . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by Def3;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by CJ00, BJ2; :: thesis: verum

end;

end;

end;

hence ((half_open_sets (a,b)) . n) ` is Element of Borel_Sets by PROB_1:def 1; :: thesis: verum

end;

hence (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets by PROB_1:def 2; :: thesis: verum

end;

then Complement (half_open_sets (a,b)) is SetSequence of Borel_Sets by PROB_1:25;
then Union (Complement (half_open_sets (a,b))) is Element of Borel_Sets by PROB_1:26;
hence Intersection (half_open_sets (a,b)) is Element of Borel_Sets by PROB_1:def 1; :: thesis: verum