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_{1}[ Nat] means (Partial_Intersection (half_open_sets (a,b))) . $1 is Element of Borel_Sets ;

A1: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

defpred S

A1: S

proof

A2:
for k being Nat st S
(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_{1}[ 0 ]
by Th4; :: thesis: verum

end;then (Partial_Intersection (half_open_sets (a,b))) . 0 = halfline_fin (a,(b + 1)) by Def1;

hence S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ; :: thesis: S_{1}[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_{1}[k + 1]
by A4, FINSUB_1:def 2; :: thesis: verum

end;assume A3: (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ; :: thesis: S

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

hence for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets ; :: thesis: verum