let AFP be AffinPlane; :: thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t
let o, a, b, x, y, z, t be Element of AFP; :: thesis: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t implies x,z // y,t )
assume ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t ) ; :: thesis: x,z // y,t
then z,x // t,y by Lm14;
hence x,z // y,t by AFF_1:13; :: thesis: verum