let V be RealLinearSpace; for v, w being Point of V holds LSeg (v,w) c= Line (v,w)
let v, w be Point of V; LSeg (v,w) c= Line (v,w)
let e be object ; TARSKI:def 3 ( not e in LSeg (v,w) or e in Line (v,w) )
assume
e in LSeg (v,w)
; 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)
; verum