:: deftheorem defines Ext_Borelsubsets_help FINANCE5:def 17 :
for A being Element of Ext_Borel_Sets holds Ext_Borelsubsets_help A = A /\ [.0,+infty.];