let V be RealLinearSpace; :: thesis: for v being Point of V holds Line (v,v) = {v}
let v be Point of V; :: thesis: Line (v,v) = {v}
for x being object holds
( x in Line (v,v) iff x = v )

proof

let x be object ; :: thesis: ( x in Line (v,v) iff x = v )
thus ( x in Line (v,v) implies x = v ) :: thesis: ( x = v implies x in Line (v,v) )

proof

assume A1: x in Line (v,v) ; :: thesis: x = v
then reconsider w = x as Point of V ;
consider r being Real such that
A2: w = ((1 - r) * v) + (r * v) by A1;
w = ((1 - r) + r) * v by A2, RLVECT_1:def 6;
hence x = v by RLVECT_1:def 8; :: thesis: verum

end;

assume x = v ; :: thesis: x in Line (v,v)
hence x in Line (v,v) by Th72; :: thesis: verum

end;

hence Line (v,v) = {v} by TARSKI:def 1; :: thesis: verum