theorem Th64: :: EUCLIDLP:64

for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds
( Line (x1,x2) = L & L is being_line )