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 & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,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 & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) implies x,z // y,t )
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: LIN o,a,b and
A4: not LIN o,a,x and
A5: LIN o,x,y and
A6: a,x // b,y and
A7: LIN o,a,z and
A8: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) ; :: thesis: x,z // y,t
consider p, p9 being Element of AFP such that
A9: not LIN o,a,p and
A10: LIN o,p,p9 and
A11: a,p // b,p9 and
A12: p,z // p9,t and
A13: LIN o,a,t by A8;

A14: now :: thesis: ( a = z implies x,z // y,t )

A15: p,a // p9,b by A11, AFF_1:4;
assume A16: a = z ; :: thesis: x,z // y,t
not LIN o,p,a by A9, AFF_1:6;
then z,x // t,y by A3, A6, A10, A12, A13, A16, A15, AFF_1:56;
hence x,z // y,t by AFF_1:4; :: thesis: verum

end;

A17: p,x // p9,y by A1, A3, A4, A5, A6, A9, A10, A11, Lm1;

A18: now :: thesis: ( z <> o & not LIN o,p,x implies x,z // y,t )

assume that
A19: z <> o and
A20: not LIN o,p,x ; :: thesis: x,z // y,t
A21: not LIN o,p,z

proof

A22: LIN o,p,o by AFF_1:7;
assume A23: LIN o,p,z ; :: thesis: contradiction
LIN o,z,a by A7, AFF_1:6;
then LIN o,p,a by A19, A23, A22, AFF_1:11;
hence contradiction by A9, AFF_1:6; :: thesis: verum

end;

LIN o,a,o by AFF_1:7;
then LIN o,z,t by A2, A7, A13, AFF_1:8;
hence x,z // y,t by A1, A5, A10, A12, A17, A20, A21, Lm1; :: thesis: verum

end;

A24: o <> x by A4, AFF_1:7;

A25: now :: thesis: ( z <> o & LIN o,p,x & a <> z implies x,z // y,t )

assume that
A26: z <> o and
A27: LIN o,p,x and
a <> z ; :: thesis: x,z // y,t

now :: thesis: ( x <> p implies x,z // y,t )

A28: LIN o,x,o by AFF_1:7;
LIN o,x,p by A27, AFF_1:6;
then A29: LIN o,p,y by A5, A24, A28, AFF_1:8;
assume A30: x <> p ; :: thesis: x,z // y,t
z,p // t,p9 by A12, AFF_1:4;
then z,x // t,y by A1, A3, A6, A7, A9, A10, A11, A13, A24, A26, A27, A30, A29, Th1;
hence x,z // y,t by AFF_1:4; :: thesis: verum

end;

hence x,z // y,t by A3, A4, A5, A6, A10, A11, A12, AFF_1:56; :: thesis: verum

end;

now :: thesis: ( z = o implies x,z // y,t )

A31: o,x // o,y by A5, AFF_1:def 1;
assume A32: z = o ; :: thesis: x,z // y,t
then t = o by A2, A7, A8, Lm7;
hence x,z // y,t by A32, A31, AFF_1:4; :: thesis: verum

end;

hence x,z // y,t by A18, A14, A25; :: thesis: verum