theorem Th11: :: EUCLID_4:11

for n being Nat
for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (x1,x2) c= Line (y1,y2)