let AFP be AffinPlane; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: ( x <> z implies x,z // y,t )

assume A11: x <> z ; :: thesis: x,z // y,t
then 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; :: thesis: verum

end;

hence x,z // y,t by AFF_1:3; :: thesis: verum