let a, b be real number ; :: thesis: for n being natural number 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 ;
AJ0: 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 Def3;
hence S₁[ 0 ] by BJ2; :: thesis: verum

end;

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

proof

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(AJ0, AJ1);
hence for n being natural number holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets ; :: thesis: verum