let V be RealLinearSpace; :: thesis: for v being Point of V holds LSeg v,v = {v}
let v be Point of V; :: thesis: LSeg v,v = {v}
thus LSeg v,v c= {v} :: according to XBOOLE_0:def 10 :: thesis: {v} c= LSeg v,v

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg v,v or a in {v} )
assume a in LSeg v,v ; :: thesis: a in {v}
then consider r being Real such that
A2: a = ((1 - r) * v) + (r * v) and
( 0 <= r & r <= 1 ) ;
a = ((1 - r) + r) * v by A2, RLVECT_1:def 9
.= v by RLVECT_1:def 9 ;
hence a in {v} by TARSKI:def 1; :: thesis: verum

end;

v in LSeg v,v by Th69;
hence {v} c= LSeg v,v by ZFMISC_1:37; :: thesis: verum