now :: thesis: for A being object st A in Family_of_halflines holds
A in Family_of_Intervals
let A be object ; :: thesis: ( A in Family_of_halflines implies A in Family_of_Intervals )
assume A in Family_of_halflines ; :: thesis: A in Family_of_Intervals
then consider r being Element of REAL such that
A1: A = halfline r by PROB_1:def 11;
A = ].-infty,r.[ by A1, PROB_1:def 10;
hence A in Family_of_Intervals by A1; :: thesis: verum
end;
hence Family_of_halflines c= Family_of_Intervals ; :: thesis: verum