:: deftheorem defines Family_of_halflines PROB_1:def 11 :
Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;