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

proof

let n be Nat; :: thesis: (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
((half_open_sets (a,b)) . nn) ` 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 A1: 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 Def1;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by A1, Th4; :: 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
A2: 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 Def1;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by A2, Th4; :: thesis: verum

end;

end;

end;

hence ((half_open_sets (a,b)) . nn) ` 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