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 object ; :: 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
A1: a = ((1 - r) * v) + (r * v) and
0 <= r and
r <= 1 ;
a = ((1 - r) + r) * v by A1, RLVECT_1:def 6
.= v by RLVECT_1:def 8 ;
hence a in {v} by TARSKI:def 1; :: thesis: verum
end;
v in LSeg (v,v) by Th68;
hence {v} c= LSeg (v,v) by ZFMISC_1:31; :: thesis: verum