let a, b be Real; :: thesis: 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 ]
proof
(Partial_Intersection (half_open_sets (a,b))) . 0 = (half_open_sets (a,b)) . 0 by PROB_3:def 1;
then (Partial_Intersection (half_open_sets (a,b))) . 0 = halfline_fin (a,(b + 1)) by Def1;
hence S1[ 0 ] by Th4; :: thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum