let b be Real; :: thesis: Intersection (ext_half_open_sets b) is Element of Ext_Borel_Sets

for n being Nat holds (Complement (ext_half_open_sets b)) . n is Element of Ext_Borel_Sets

then Union (Complement (ext_half_open_sets b)) is Element of Ext_Borel_Sets by PROB_1:26;

hence Intersection (ext_half_open_sets b) is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum

for n being Nat holds (Complement (ext_half_open_sets b)) . n is Element of Ext_Borel_Sets

proof

then
Complement (ext_half_open_sets b) is SetSequence of Ext_Borel_Sets
by PROB_1:25;
let n be Nat; :: thesis: (Complement (ext_half_open_sets b)) . n is Element of Ext_Borel_Sets

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

((ext_half_open_sets b) . nn) ` is Element of Ext_Borel_Sets

end;reconsider nn = n as Element of NAT by ORDINAL1:def 12;

((ext_half_open_sets b) . nn) ` is Element of Ext_Borel_Sets

proof

hence
(Complement (ext_half_open_sets b)) . n is Element of Ext_Borel_Sets
by PROB_1:def 2; :: thesis: verum
(ext_half_open_sets b) . n is Element of Ext_Borel_Sets

end;proof
end;

hence
((ext_half_open_sets b) . nn) ` is Element of Ext_Borel_Sets
by PROB_1:def 1; :: thesis: verumper cases
( n = 0 or ex k being Nat st n = k + 1 )
by NAT_1:6;

end;

suppose A1:
n = 0
; :: thesis: (ext_half_open_sets b) . n is Element of Ext_Borel_Sets

(ext_half_open_sets b) . 0 = ].(b - 1),+infty.]
by Def300;

hence (ext_half_open_sets b) . n is Element of Ext_Borel_Sets by A1, Th3; :: thesis: verum

end;hence (ext_half_open_sets b) . n is Element of Ext_Borel_Sets by A1, Th3; :: thesis: verum

suppose
ex k being Nat st n = k + 1
; :: thesis: (ext_half_open_sets b) . n is Element of Ext_Borel_Sets

then consider k being Nat such that

A2: n = k + 1 ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(ext_half_open_sets b) . (k + 1) = ].(b - (1 / (k + 1))),+infty.] by Def300;

hence (ext_half_open_sets b) . n is Element of Ext_Borel_Sets by A2, Th3; :: thesis: verum

end;A2: n = k + 1 ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(ext_half_open_sets b) . (k + 1) = ].(b - (1 / (k + 1))),+infty.] by Def300;

hence (ext_half_open_sets b) . n is Element of Ext_Borel_Sets by A2, Th3; :: thesis: verum

then Union (Complement (ext_half_open_sets b)) is Element of Ext_Borel_Sets by PROB_1:26;

hence Intersection (ext_half_open_sets b) is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum