let AFP be AffinPlane; :: thesis: for a, b, o, t, x, y, z being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t
let a, b, o, t, x, y, z be Element of AFP; :: thesis: ( AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t implies x,z // y,t )
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: LIN o,a,b and
A4: LIN o,a,x and
A5: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and
A6: not LIN o,a,z and
A7: LIN o,z,t and
A8: a,z // b,t ; :: thesis: x,z // y,t
z,x // t,y by A1, A2, A3, A4, A5, A6, A7, A8, Lm14;
hence x,z // y,t by AFF_1:4; :: thesis: verum