let AFP be AffinPlane; for o, a, b, x, y, r being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & 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 ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds
y = r
let o, a, b, x, y, r be Element of AFP; ( o <> a & LIN o,a,b & AFP is Desarguesian & 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 ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) implies y = r )
assume that
A1:
o <> a
and
A2:
LIN o,a,b
and
A3:
AFP is Desarguesian
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:
ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r )
; y = r
consider q, q9 being Element of AFP such that
A7:
not LIN o,a,q
and
A8:
LIN o,q,q9
and
A9:
a,q // b,q9
and
A10:
q,x // q9,r
and
A11:
LIN o,a,r
by A6;
A12:
o <> q
by A7, AFF_1:16;
consider p, p9 being Element of AFP such that
A13:
not LIN o,a,p
and
A14:
LIN o,p,p9
and
A15:
a,p // b,p9
and
A16:
p,x // p9,y
and
A17:
LIN o,a,y
by A5;
A18:
( a = x implies y = r )
proof
A19:
q,
a // q9,
b
by A9, AFF_1:13;
A20:
not
LIN o,
q,
a
by A7, AFF_1:15;
A21:
p,
a // p9,
b
by A15, AFF_1:13;
assume A22:
a = x
;
y = r
not
LIN o,
p,
a
by A13, AFF_1:15;
then
b = y
by A2, A14, A16, A17, A22, A21, AFF_1:70;
hence
y = r
by A2, A8, A10, A11, A22, A20, A19, AFF_1:70;
verum
end;
A23:
o <> p
by A13, AFF_1:16;
A24:
( a <> b & a <> x & p <> q & o <> x implies y = r )
proof
assume that
a <> b
and
a <> x
and A25:
p <> q
and A26:
o <> x
;
y = r
A27:
now set K =
Line o,
p;
set A =
Line o,
a;
A28:
LIN o,
q,
o
by AFF_1:16;
A29:
o in Line o,
a
by AFF_1:26;
A30:
p in Line o,
p
by AFF_1:26;
A31:
o in Line o,
p
by AFF_1:26;
A32:
Line o,
a is
being_line
by A1, AFF_1:def 3;
A33:
x in Line o,
a
by A4, AFF_1:def 2;
r in Line o,
a
by A11, AFF_1:def 2;
then A34:
LIN o,
x,
r
by A32, A29, A33, AFF_1:33;
A35:
x,
p // y,
p9
by A16, AFF_1:13;
assume A36:
LIN o,
p,
q
;
y = rthen
LIN o,
q,
p
by AFF_1:15;
then
LIN o,
p,
q9
by A8, A12, A28, AFF_1:17;
then
x,
q // y,
q9
by A2, A3, A4, A13, A14, A15, A17, A9, A12, A25, A26, A36, A35, Th1;
then A37:
q,
x // q9,
y
by AFF_1:13;
A38:
Line o,
p is
being_line
by A23, AFF_1:def 3;
A39:
q in Line o,
p
by A36, AFF_1:def 2;
A40:
not
LIN o,
q,
x
proof
assume A41:
LIN o,
q,
x
;
contradiction
Line o,
p = Line o,
q
by A12, A38, A31, A39, AFF_1:38;
then
x in Line o,
p
by A41, AFF_1:def 2;
then A42:
p in Line o,
a
by A26, A32, A29, A33, A38, A31, A30, AFF_1:30;
A43:
a in Line o,
a
by AFF_1:26;
Line o,
a is
being_line
by A1, AFF_1:def 3;
hence
contradiction
by A13, A29, A43, A42, AFF_1:33;
verum
end;
y in Line o,
a
by A17, AFF_1:def 2;
then
LIN o,
x,
y
by A32, A29, A33, AFF_1:33;
hence
y = r
by A8, A10, A37, A40, A34, AFF_1:70;
verum end;
now A44:
not
LIN o,
p,
x
proof
assume
LIN o,
p,
x
;
contradiction
then A45:
LIN o,
x,
p
by AFF_1:15;
LIN o,
a,
o
by AFF_1:16;
hence
contradiction
by A4, A13, A26, A45, AFF_1:20;
verum
end; set K =
Line o,
q;
set A =
Line o,
a;
assume A46:
not
LIN o,
p,
q
;
y = rA47:
o in Line o,
a
by AFF_1:26;
A48:
q in Line o,
q
by AFF_1:26;
A49:
o in Line o,
q
by AFF_1:26;
A50:
Line o,
a is
being_line
by A1, AFF_1:def 3;
A51:
x in Line o,
a
by A4, AFF_1:def 2;
A52:
y in Line o,
a
by A17, AFF_1:def 2;
then A53:
LIN o,
x,
y
by A50, A47, A51, AFF_1:33;
A54:
Line o,
q is
being_line
by A12, AFF_1:def 3;
A55:
not
LIN o,
q,
x
proof
assume
LIN o,
q,
x
;
contradiction
then
x in Line o,
q
by AFF_1:def 2;
then A56:
q in Line o,
a
by A26, A50, A47, A51, A54, A49, A48, AFF_1:30;
A57:
a in Line o,
a
by AFF_1:26;
Line o,
a is
being_line
by A1, AFF_1:def 3;
hence
contradiction
by A7, A47, A57, A56, AFF_1:33;
verum
end;
r in Line o,
a
by A11, AFF_1:def 2;
then A58:
LIN o,
x,
r
by A50, A47, A51, AFF_1:33;
A59:
LIN o,
x,
y
by A50, A47, A51, A52, AFF_1:33;
p,
q // p9,
q9
by A2, A3, A13, A14, A15, A7, A8, A9, Lm1;
then
q,
x // q9,
y
by A3, A14, A16, A8, A46, A44, A53, Lm1;
hence
y = r
by A8, A10, A55, A59, A58, AFF_1:70;
verum end;
hence
y = r
by A27;
verum
end;
A60:
o <> a
by A13, AFF_1:16;
A61:
( p = q & o <> x implies y = r )
proof
assume that A62:
p = q
and A63:
o <> x
;
y = r
A64:
not
LIN o,
p,
x
proof
assume
LIN o,
p,
x
;
contradiction
then A65:
LIN o,
x,
p
by AFF_1:15;
A66:
LIN o,
x,
o
by AFF_1:16;
LIN o,
x,
a
by A4, AFF_1:15;
hence
contradiction
by A13, A63, A66, A65, AFF_1:17;
verum
end;
A67:
LIN o,
a,
o
by AFF_1:16;
then A68:
LIN o,
x,
y
by A4, A17, A60, AFF_1:17;
A69:
LIN o,
x,
r
by A4, A11, A60, A67, AFF_1:17;
p9 = q9
by A2, A13, A14, A15, A8, A9, A62, AFF_1:70;
hence
y = r
by A14, A16, A10, A62, A68, A69, A64, AFF_1:70;
verum
end;
A70:
( o = x implies y = r )
( a = b implies y = r )
hence
y = r
by A70, A61, A18, A24; verum