let V be RealLinearSpace; :: thesis: for p, q being Element of V holds LSeg (p,q) c= halfline (p,q)
let p, q be Element of V; :: thesis: LSeg (p,q) c= halfline (p,q)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (p,q) or a in halfline (p,q) )
assume a in LSeg (p,q) ; :: thesis: a in halfline (p,q)
then ex r being Real st
( 0 <= r & r <= 1 & a = ((1 - r) * p) + (r * q) ) by RLTOPSP1:76;
hence a in halfline (p,q) ; :: thesis: verum