let AFP be 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
let a, b, o, p, p9, q, q9, x, y be Element of AFP; ( 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 implies x,q // y,q9 )
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,p9
and
A6:
LIN o,p,q
and
A7:
LIN o,p,q9
and
A8:
p <> q
and
A9:
o <> q
and
A10:
o <> x
and
A11:
a,p // b,p9
and
A12:
a,q // b,q9
and
A13:
x,p // y,p9
and
A14:
AFP is Desarguesian
; x,q // y,q9
set B9 = Line (o,p);
A15:
o in Line (o,p)
by AFF_1:15;
A16:
o <> p
by A1, AFF_1:7;
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:1;
A20:
Line (o,p) is being_line
by A16, AFF_1:def 3;
A21:
q9 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,q9
by A20, A15, A21, AFF_1:21;
set A = Line (o,a);
o <> a
by A1, AFF_1:7;
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 // p9,b
by A11, AFF_1:4;
A26:
not LIN o,p,a
by A1, AFF_1:6;
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:49;
A30:
x in Line (x,p)
by AFF_1:15;
A31:
M is being_line
by A29, AFF_1:36;
A32:
p in Line (x,p)
by AFF_1:15;
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
;
contradiction
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:18;
hence
contradiction
by A1, A32, AFF_1:def 2;
verum
end;
A36:
o in Line (o,a)
by AFF_1:15;
not o,d // M
proof
assume
o,
d // M
;
contradiction
then
o,
d // Line (
x,
p)
by A29, AFF_1:43;
then
d,
o // Line (
x,
p)
by AFF_1:34;
then
o in Line (
x,
p)
by A27, A33, AFF_1:23;
then
Line (
o,
a)
= Line (
x,
p)
by A10, A27, A30, A23, A36, A34, AFF_1:18;
hence
contradiction
by A1, A32, AFF_1:def 2;
verum
end;
then consider d9 being Element of AFP such that
A37:
d9 in M
and
A38:
LIN o,d,d9
by A31, AFF_1:59;
A39:
d,x // d9,y
by A30, A33, A28, A29, A37, AFF_1:39;
A40:
p in Line (o,p)
by AFF_1:15;
A41:
not LIN o,d,q
proof
assume
LIN o,
d,
q
;
contradiction
then A42:
LIN o,
q,
d
by AFF_1:6;
A43:
LIN o,
q,
o
by AFF_1:7;
LIN o,
q,
p
by A6, AFF_1:6;
then
LIN o,
p,
d
by A9, A43, A42, AFF_1:8;
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:18;
then
Line (
o,
a)
= Line (
o,
p)
by A10, A27, A30, A23, A36, A34, A15, AFF_1:18;
hence
contradiction
by A1, A40, AFF_1:def 2;
verum
end;
A44:
not LIN o,d,x
proof
assume
LIN o,
d,
x
;
contradiction
then
LIN o,
x,
d
by AFF_1:6;
then
d in Line (
o,
a)
by A10, A23, A36, A34, AFF_1:25;
then
Line (
o,
a)
= Line (
x,
p)
by A18, A27, A30, A33, A23, A34, AFF_1:18;
hence
contradiction
by A1, A32, AFF_1:def 2;
verum
end;
A45:
not LIN o,p,d
proof
assume
LIN o,
p,
d
;
contradiction
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:18;
hence
contradiction
by A27, A30, A33, A15, A44, AFF_1:21;
verum
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
;
contradiction
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:18;
hence
contradiction
by A1, A40, AFF_1:def 2;
verum
end;
x in Line (o,a)
by A3, AFF_1:def 2;
then A48:
LIN o,x,y
by A23, A36, A24, AFF_1:21;
x,p // Line (x,p)
by A27, A30, A32, AFF_1:23;
then
x,p // M
by A29, AFF_1:43;
then
y,p9 // M
by A1, A3, A13, AFF_1:32;
then
p9 in M
by A28, A31, AFF_1:23;
then
p,d // p9,d9
by A32, A33, A29, A37, AFF_1:39;
then
a,d // b,d9
by A2, A5, A14, A38, A45, A26, A25, Lm1;
then
d,q // d9,q9
by A2, A12, A14, A38, A47, A35, A22, Lm1;
hence
x,q // y,q9
by A14, A38, A39, A41, A44, A22, A48, Lm1; verum