let a, b be Real; for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
defpred S1[ Nat] means (Partial_Intersection (half_open_sets (a,b))) . $1 is Element of Borel_Sets ;
A1:
S1[ 0 ]
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
(Partial_Intersection (half_open_sets (a,b))) . k is
Element of
Borel_Sets
;
S1[k + 1]
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
(Partial_Intersection (half_open_sets (a,b))) . (k + 1) = ((Partial_Intersection (half_open_sets (a,b))) . k) /\ ((half_open_sets (a,b)) . (k + 1))
by PROB_3:def 1;
then A4:
(Partial_Intersection (half_open_sets (a,b))) . (k + 1) = ((Partial_Intersection (half_open_sets (a,b))) . k) /\ (halfline_fin (a,(b + (1 / (k + 1)))))
by Def1;
(
[.a,(b + (1 / (k + 1))).[ is
Element of
Borel_Sets &
(Partial_Intersection (half_open_sets (a,b))) . k is
Element of
Borel_Sets )
by Th4, A3;
hence
S1[
k + 1]
by A4, FINSUB_1:def 2;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
; verum