let b be Real; :: thesis:
for n being Nat holds () . n is Element of Ext_Borel_Sets
proof
let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
((ext_half_open_sets b) . nn) ` is Element of Ext_Borel_Sets
proof
(ext_half_open_sets b) . n is Element of Ext_Borel_Sets
proof
per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
suppose ex k being Nat st n = k + 1 ; :: thesis:
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 ; :: thesis: verum
end;
end;
end;
hence ((ext_half_open_sets b) . nn) ` is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum
end;
hence (Complement ) . n is Element of Ext_Borel_Sets by PROB_1:def 2; :: thesis: verum
end;
then Complement is SetSequence of Ext_Borel_Sets by PROB_1:25;
then Union () is Element of Ext_Borel_Sets by PROB_1:26;
hence Intersection is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum