let V be RealLinearSpace; :: thesis: for p1, p2 being Point of V holds halfline (p1,p2) c= Line (p1,p2)
let p1, p2 be Point of V; :: thesis: halfline (p1,p2) c= Line (p1,p2)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in halfline (p1,p2) or e in Line (p1,p2) )
assume e in halfline (p1,p2) ; :: thesis: e in Line (p1,p2)
then ex r being Real st
( e = ((1 - r) * p1) + (r * p2) & 0 <= r ) ;
hence e in Line (p1,p2) ; :: thesis: verum