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