let AFP be AffinPlane; :: thesis:
let o, a, p, b, x, y, p', q, q' be Element of AFP; :: thesis:
assume that
A1: not LIN o,a,p and
A2: LIN o,a,b and
A3: LIN o,a,x and
A4: LIN o,a,y and
A5: LIN o,p,p' and
A6: LIN o,p,q and
A7: LIN o,p,q' and
A8: p <> q and
A9: o <> q and
A10: o <> x and
A11: a,p // b,p' and
A12: a,q // b,q' and
A13: x,p // y,p' and
A14: AFP is Desarguesian ; :: thesis:
set B' = Line o,p;
A15: o in Line o,p by AFF_1:26;
A16: o <> p by A1, AFF_1:16;
then consider d being Element of AFP such that
A17: LIN x,p,d and
A18: d <> x and
A19: d <> p by A6, A8, A9, TRANSLAC:2;
A20: Line o,p is being_line by A16, AFF_1:def 3;
A21: q' in Line o,p by A7, AFF_1:def 2;
q in Line o,p by A6, AFF_1:def 2;
then A22: LIN o,q,q' by A20, A15, A21, AFF_1:33;
set A = Line o,a;
o <> a by A1, AFF_1:16;
then A23: Line o,a is being_line by AFF_1:def 3;
A24: y in Line o,a by A4, AFF_1:def 2;
A25: p,a // p',b by A11, AFF_1:13;
A26: not LIN o,p,a by A1, AFF_1:15;
set K = Line x,p;
A27: Line x,p is being_line by A1, A3, AFF_1:def 3;
then consider M being Subset of AFP such that
A28: y in M and
A29: Line x,p // M by AFF_1:63;
A30: x in Line x,p by AFF_1:26;
A31: M is being_line by A29, AFF_1:50;
A32: p in Line x,p by AFF_1:26;
A33: d in Line x,p by A17, AFF_1:def 2;
A34: x in Line o,a by A3, AFF_1:def 2;
A35: not LIN o,a,d

proof

assume LIN o,a,d ; :: thesis:
then d in Line o,a by AFF_1:def 2;
then Line o,a = Line x,p by A18, A27, A30, A33, A23, A34, AFF_1:30;
hence contradiction by A1, A32, AFF_1:def 2; :: thesis:

end;

A36: o in Line o,a by AFF_1:26;
not o,d // M

proof

assume o,d // M ; :: thesis:
then o,d // Line x,p by A29, AFF_1:57;
then d,o // Line x,p by AFF_1:48;
then o in Line x,p by A27, A33, AFF_1:37;
then Line o,a = Line x,p by A10, A27, A30, A23, A36, A34, AFF_1:30;
hence contradiction by A1, A32, AFF_1:def 2; :: thesis:

end;

then consider d' being Element of AFP such that
A37: d' in M and
A38: LIN o,d,d' by A31, AFF_1:73;
A39: d,x // d',y by A30, A33, A28, A29, A37, AFF_1:53;
A40: p in Line o,p by AFF_1:26;
A41: not LIN o,d,q

proof

assume LIN o,d,q ; :: thesis:
then A42: LIN o,q,d by AFF_1:15;
A43: LIN o,q,o by AFF_1:16;
LIN o,q,p by A6, AFF_1:15;
then LIN o,p,d by A9, A43, A42, AFF_1:17;
then d in Line o,p by AFF_1:def 2;
then Line o,p = Line x,p by A19, A27, A32, A33, A20, A40, AFF_1:30;
then Line o,a = Line o,p by A10, A27, A30, A23, A36, A34, A15, AFF_1:30;
hence contradiction by A1, A40, AFF_1:def 2; :: thesis:

end;

A44: not LIN o,d,x

proof

assume LIN o,d,x ; :: thesis:
then LIN o,x,d by AFF_1:15;
then d in Line o,a by A10, A23, A36, A34, AFF_1:39;
then Line o,a = Line x,p by A18, A27, A30, A33, A23, A34, AFF_1:30;
hence contradiction by A1, A32, AFF_1:def 2; :: thesis:

end;

A45: not LIN o,p,d

proof

assume LIN o,p,d ; :: thesis:
then d in Line o,p by AFF_1:def 2;
then Line x,p = Line o,p by A19, A27, A32, A33, A20, A40, AFF_1:30;
hence contradiction by A27, A30, A33, A15, A44, AFF_1:33; :: thesis:

end;

A46: q in Line o,p by A6, AFF_1:def 2;
A47: not LIN o,a,q

proof

assume LIN o,a,q ; :: thesis:
then q in Line o,a by AFF_1:def 2;
then Line o,a = Line o,p by A9, A23, A36, A20, A15, A46, AFF_1:30;
hence contradiction by A1, A40, AFF_1:def 2; :: thesis:

end;

x in Line o,a by A3, AFF_1:def 2;
then A48: LIN o,x,y by A23, A36, A24, AFF_1:33;
x,p // Line x,p by A27, A30, A32, AFF_1:37;
then x,p // M by A29, AFF_1:57;
then y,p' // M by A1, A3, A13, AFF_1:46;
then p' in M by A28, A31, AFF_1:37;
then p,d // p',d' by A32, A33, A29, A37, AFF_1:53;
then a,d // b,d' by A2, A5, A14, A38, A45, A26, A25, Lm1;
then d,q // d',q' by A2, A12, A14, A38, A47, A35, A22, Lm1;
hence x,q // y,q' by A14, A38, A39, A41, A44, A22, A48, Lm1; :: thesis: