:: deftheorem defines ExtBorelsubsets FINANCE5:def 18 :
ExtBorelsubsets = { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;