let AFP be AffinPlane; for a, b, o, t, x, y, z being Element of AFP st o <> a & 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 ) & 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; ( o <> a & 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 ) & 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:
o <> a
and
A2:
LIN o,a,x
and
A3:
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
A4:
LIN o,a,z
and
A5:
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
set A = Line (o,a);
A6:
x in Line (o,a)
by A2, AFF_1:def 2;
A7:
z in Line (o,a)
by A4, AFF_1:def 2;
A8:
y in Line (o,a)
by A3, AFF_1:def 2;
A9:
t in Line (o,a)
by A5, AFF_1:def 2;
A10:
Line (o,a) is being_line
by A1, AFF_1:def 3;
now ( x <> z implies x,z // y,t )assume A11:
x <> z
;
x,z // y,tthen
Line (
o,
a)
= Line (
x,
z)
by A10, A6, A7, AFF_1:24;
hence
x,
z // y,
t
by A8, A9, A11, AFF_1:22;
verum end;
hence
x,z // y,t
by AFF_1:3; verum