let AFP be AffinPlane; 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; ( 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 )
; 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 ( a = z implies x,z // y,t )A15:
p,
a // p9,
b
by A11, AFF_1:4;
assume A16:
a = z
;
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;
verum end;
A17:
p,x // p9,y
by A1, A3, A4, A5, A6, A9, A10, A11, Lm1;
A18:
now ( z <> o & not LIN o,p,x implies x,z // y,t )assume that A19:
z <> o
and A20:
not
LIN o,
p,
x
;
x,z // y,tA21:
not
LIN o,
p,
z
proof
A22:
LIN o,
p,
o
by AFF_1:7;
assume A23:
LIN o,
p,
z
;
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;
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;
verum end;
A24:
o <> x
by A4, AFF_1:7;
A25:
now ( 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
;
x,z // y,tnow ( 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
;
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;
verum end; hence
x,
z // y,
t
by A3, A4, A5, A6, A10, A11, A12, AFF_1:56;
verum end;
now ( z = o implies x,z // y,t )A31:
o,
x // o,
y
by A5, AFF_1:def 1;
assume A32:
z = o
;
x,z // y,tthen
t = o
by A2, A7, A8, Lm7;
hence
x,
z // y,
t
by A32, A31, AFF_1:4;
verum end;
hence
x,z // y,t
by A18, A14, A25; verum