let b be Real; :: thesis: Intersection (ext_left_closed_sets b) is Element of Ext_Borel_Sets
for n being Nat holds (Complement (ext_left_closed_sets b)) . n is Element of Ext_Borel_Sets
proof
let n be Nat; :: thesis: (Complement (ext_left_closed_sets b)) . n is Element of Ext_Borel_Sets
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
((ext_left_closed_sets b) . nn) ` is Element of Ext_Borel_Sets
proof
(ext_left_closed_sets b) . n is Element of Ext_Borel_Sets hence ((ext_left_closed_sets b) . nn) ` is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum
end;
hence (Complement (ext_left_closed_sets b)) . n is Element of Ext_Borel_Sets by PROB_1:def 2; :: thesis: verum
end;
then Complement (ext_left_closed_sets b) is SetSequence of Ext_Borel_Sets by PROB_1:25;
then Union (Complement (ext_left_closed_sets b)) is Element of Ext_Borel_Sets by PROB_1:26;
hence Intersection (ext_left_closed_sets b) is Element of Ext_Borel_Sets by PROB_1:def 1; :: thesis: verum