halfline_fin (a,r) = [.a,r.[ ;
hence halfline_fin (a,r) is Subset of REAL ; :: thesis: verum