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