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 S₁[ Nat] means (Partial_Intersection (half_open_sets (a,b))) . $1 is Element of Borel_Sets ;
A1: S₁[ 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 S₁[ 0 ] by Th4; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ; :: thesis: S₁[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 S₁[k + 1] by A4, FINSUB_1:def 2; :: thesis: verum

end;

for k being Nat holds S₁[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