theorem Th9: :: EUCLID_4:9

for n being Nat
for x1, x2 being Element of REAL n holds
( x1 in Line (x1,x2) & x2 in Line (x1,x2) )