let AFP be AffinPlane; :: thesis: for o, a, b, x being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex y 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, x be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b implies ex y 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 A1: ( o <> a & o <> b & LIN o,a,b ) ; :: thesis: ex y 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 ) ) )

A2: now

assume A3: not LIN o,a,x ; :: thesis: ex y 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 ) ) )
o,a // o,b by A1, AFF_1:def 1;
then a,o // o,b by AFF_1:13;
then consider y being Element of AFP such that
A4: ( x,o // o,y & x,a // b,y ) by A1, DIRAF:47;
o,x // o,y by A4, AFF_1:13;
then ( LIN o,x,y & a,x // b,y ) by A4, AFF_1:13, AFF_1:def 1;
hence ex y 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 ) ) ) by A3; :: thesis: verum

end;

now

assume A5: LIN o,a,x ; :: thesis: ex y 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 ) ) )
consider p being Element of AFP such that
A6: not LIN o,a,p by A1, AFF_1:22;
A7: ( o <> p & o <> a & a <> p ) by A6, AFF_1:16;
set M = Line o,a;
set K = Line o,p;
set A = Line a,p;
A8: ( o in Line o,a & a in Line o,a & o in Line o,p & p in Line o,p & a in Line a,p & p in Line a,p ) by AFF_1:26;
A9: x in Line o,a by A5, AFF_1:def 2;
A10: ( Line o,a is being_line & Line o,p is being_line & Line a,p is being_line ) by A7, AFF_1:def 3;
then consider B' being Subset of AFP such that
A11: ( b in B' & Line a,p // B' ) by AFF_1:63;
A12: B' is being_line by A11, AFF_1:50;
not B' // Line o,p

proof

assume B' // Line o,p ; :: thesis: contradiction
then Line a,p // Line o,p by A11, AFF_1:58;
then Line a,p = Line o,p by A8, AFF_1:59;
hence contradiction by A6, A8, A10, AFF_1:33; :: thesis: verum

end;

then consider p' being Element of AFP such that
A13: ( p' in B' & p' in Line o,p ) by A10, A12, AFF_1:72;
set C = Line p,x;
A14: ( p in Line p,x & x in Line p,x ) by AFF_1:26;
A15: Line p,x is being_line by A5, A6, AFF_1:def 3;
then consider D being Subset of AFP such that
A16: ( p' in D & Line p,x // D ) by AFF_1:63;
A17: D is being_line by A16, AFF_1:50;
not D // Line o,a

proof

assume D // Line o,a ; :: thesis: contradiction
then Line p,x // Line o,a by A16, AFF_1:58;
then Line p,x = Line o,a by A9, A14, AFF_1:59;
hence contradiction by A6, A8, A14, A15, AFF_1:33; :: thesis: verum

end;

then consider y being Element of AFP such that
A18: ( y in D & y in Line o,a ) by A10, A17, AFF_1:72;
( LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) by A8, A10, A11, A13, A14, A16, A18, AFF_1:33, AFF_1:53;
hence ex y 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 ) ) ) by A5, A6; :: thesis: verum

end;

hence ex y 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 ) ) ) by A2; :: thesis: verum