:: deftheorem defines Family_of_halflines2 FINANCE2:def 1 :
Family_of_halflines2 = { (right_closed_halfline r) where r is Element of REAL : verum } ;