let AFP be AffinPlane; :: thesis: for o, a, b, y being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex x being Element of AFP st
( ( 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 ) ) )
let o, a, b, y be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b implies ex x being Element of AFP st
( ( 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 ) ) ) )
assume ( o <> a & o <> b & LIN o,a,b ) ; :: thesis: ex x being Element of AFP st
( ( 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 ) ) )
then A1: ( o <> b & o <> a & LIN o,b,a ) by AFF_1:15;
then consider x being Element of AFP such that
A2: ( ( 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 ) ) ) by Lm8;
( ( 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 ) ) ) by A1, A2, Lm6;
hence ex x being Element of AFP st
( ( 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 ) ) ) ; :: thesis: verum