theorem Th30: :: EUCLIDLP:30

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