theorem Th37: :: EUCLID12:49

for A, B being Point of (TOP-REAL 2)
for L being Element of line_of_REAL 2 st L is being_line & A in L & B in L & A <> B holds
L = Line (A,B)