let a be Real; :: thesis: {a} is Element of Ext_Borel_Sets

[.a,a.] is Element of Ext_Borel_Sets by Th70;

hence {a} is Element of Ext_Borel_Sets by XXREAL_1:17; :: thesis: verum

[.a,a.] is Element of Ext_Borel_Sets by Th70;

hence {a} is Element of Ext_Borel_Sets by XXREAL_1:17; :: thesis: verum