:: deftheorem defines Ext_Family_of_halflines FINANCE5:def 12 :
Ext_Family_of_halflines = { [.-infty,r.] where r is Real : verum } ;