set v = the Point of V;
take Line ( the Point of V, the Point of V) ; :: thesis: Line ( the Point of V, the Point of V) is being_line
take the Point of V ; :: according to RLTOPSP1:def 15 :: thesis: ex x2 being Element of V st Line ( the Point of V, the Point of V) = Line ( the Point of V,x2)
take the Point of V ; :: thesis: Line ( the Point of V, the Point of V) = Line ( the Point of V, the Point of V)
thus Line ( the Point of V, the Point of V) = Line ( the Point of V, the Point of V) ; :: thesis: verum