let AFP be AffinPlane; :: thesis: for a, b, o, r, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( 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 ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds
x = r
let a, b, o, r, x, y be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( 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 ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) implies x = r )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: AFP is Desarguesian and
A5: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( 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 ) ) ) and
A6: ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) ; :: thesis: x = r
A7: ( ( not LIN o,b,y & LIN o,y,r & b,y // a,r ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,r & LIN o,b,r ) ) ) by A1, A2, A3, A6, Lm6;
A8: LIN o,b,a by A3, AFF_1:6;
( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) by A1, A2, A3, A5, Lm6;
hence x = r by A2, A4, A8, A7, Lm11, AFF_1:56; :: thesis: verum