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

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

for n being Nat holds (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets

proof

then
Complement (half_open_sets (a,b)) is SetSequence of Borel_Sets
by PROB_1:25;
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

end;reconsider nn = n as Element of NAT by ORDINAL1:def 12;

((half_open_sets (a,b)) . nn) ` is Element of Borel_Sets

proof

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

end;proof
end;

hence
((half_open_sets (a,b)) . nn) ` is Element of Borel_Sets
by PROB_1:def 1; :: thesis: verumper cases
( n = 0 or ex k being Nat st n = k + 1 )
by NAT_1:6;

end;

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;hence (half_open_sets (a,b)) . n is Element of Borel_Sets by A1, Th4; :: thesis: verum

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

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