theorem Th1: :: HOMOTHET:1

for AFP being AffinPlane
for a, b, o, p, p9, q, q9, x, y being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds
x,q // y,q9