let AFP be AffinPlane; :: thesis: for o, a, b, x, y, z, t being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,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: ( o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,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: ( o <> a & o <> b & LIN o,a,b ) and
A2: ( LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) and
A3: ( 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 ) ) ; :: thesis: x,z // y,t
set A = Line o,a;
A4: Line o,a is being_line by A1, AFF_1:def 3;
A5: ( x in Line o,a & y in Line o,a & z in Line o,a & t in Line o,a ) by A2, A3, AFF_1:def 2;

now

assume A6: x <> z ; :: thesis: x,z // y,t
then Line o,a = Line x,z by A4, A5, AFF_1:38;
hence x,z // y,t by A5, A6, AFF_1:36; :: thesis: verum

end;

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