theorem Th80: :: RLTOPSP1:80

for V being RealLinearSpace
for L being line of V
for x1, x2 being Element of V st x1 <> x2 & x1 in L & x2 in L holds
L = Line (x1,x2)