theorem :: FINANCE5:22

REAL is Element of Ext_Borel_Sets