let A be Subset of V; :: thesis: ( A = {v} implies A is being_line )
assume A1: A = {v} ; :: thesis: A is being_line
take v ; :: according to RLTOPSP1:def 15 :: thesis: ex x2 being Element of V st A = Line (v,x2)
take v ; :: thesis: A = Line (v,v)
thus A = Line (v,v) by A1, Th77; :: thesis: verum