let AFP be AffinPlane; :: thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) holds
x,z // y,t
let o, a, b, x, y, z, t be Element of AFP; :: thesis: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) implies x,z // y,t )
assume that
A1:
AFP is Desarguesian
and
A2:
( o <> a & o <> b & LIN o,a,b )
and
A3:
( not LIN o,a,x & LIN o,x,y & a,x // b,y )
and
A4:
LIN o,a,z
and
A5:
ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t )
; :: thesis: x,z // y,t
consider p, p' being Element of AFP such that
A6:
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t )
by A5;
A7:
p,x // p',y
by A1, A2, A3, A6, Lm1;
A8:
( o <> a & o <> x & o <> p )
by A3, A6, AFF_1:16;
A9:
now assume A10:
z = o
;
:: thesis: x,z // y,tthen A11:
t = o
by A2, A4, A5, Lm7;
o,
x // o,
y
by A3, AFF_1:def 1;
hence
x,
z // y,
t
by A10, A11, AFF_1:13;
:: thesis: verum end;
A12:
now assume A13:
(
z <> o & not
LIN o,
p,
x )
;
:: thesis: x,z // y,tA14:
not
LIN o,
p,
z
proof
assume
LIN o,
p,
z
;
:: thesis: contradiction
then
(
LIN o,
p,
o &
LIN o,
p,
z &
LIN o,
z,
a )
by A4, AFF_1:15, AFF_1:16;
then
LIN o,
p,
a
by A13, AFF_1:20;
hence
contradiction
by A6, AFF_1:15;
:: thesis: verum
end;
LIN o,
z,
t
proof
(
LIN o,
a,
o &
LIN o,
a,
z &
LIN o,
a,
t )
by A4, A6, AFF_1:16;
hence
LIN o,
z,
t
by A2, AFF_1:17;
:: thesis: verum
end; hence
x,
z // y,
t
by A1, A3, A6, A7, A13, A14, Lm1;
:: thesis: verum end;
A15:
now assume A16:
a = z
;
:: thesis: x,z // y,tA17:
not
LIN o,
p,
a
by A6, AFF_1:15;
p,
a // p',
b
by A6, AFF_1:13;
then
z,
x // t,
y
by A2, A3, A6, A16, A17, AFF_1:70;
hence
x,
z // y,
t
by AFF_1:13;
:: thesis: verum end;
now assume A18:
(
z <> o &
LIN o,
p,
x &
a <> z )
;
:: thesis: x,z // y,tnow assume A19:
x <> p
;
:: thesis: x,z // y,t
(
LIN o,
x,
o &
LIN o,
x,
p )
by A18, AFF_1:15, AFF_1:16;
then A20:
(
LIN o,
p,
x &
LIN o,
p,
y &
LIN o,
p,
p' )
by A3, A6, A8, A18, AFF_1:17;
z,
p // t,
p'
by A6, AFF_1:13;
then
z,
x // t,
y
by A1, A2, A3, A4, A6, A8, A18, A19, A20, Th1;
hence
x,
z // y,
t
by AFF_1:13;
:: thesis: verum end; hence
x,
z // y,
t
by A2, A3, A6, AFF_1:70;
:: thesis: verum end;
hence
x,z // y,t
by A9, A12, A15; :: thesis: verum