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