let AFP be AffinPlane; :: thesis: for o, a, b, x being Element of AFP st o <> a & 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, 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 ) ) )
let o, a, b, x be Element of AFP; :: thesis: ( o <> a & 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, 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 ) ) ) )
assume that
A1: o <> a and
A2: 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, 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 ) ) )

A3: now

consider p being Element of AFP such that
A4: not LIN o,a,p by A1, AFF_1:22;
set K = Line o,p;
o <> p by A4, AFF_1:16;
then A5: Line o,p is being_line by AFF_1:def 3;
set A = Line a,p;
a <> p by A4, AFF_1:16;
then Line a,p is being_line by AFF_1:def 3;
then consider B9 being Subset of AFP such that
A6: b in B9 and
A7: Line a,p // B9 by AFF_1:63;
A8: B9 is being_line by A7, AFF_1:50;
A9: a in Line a,p by AFF_1:26;
A10: p in Line o,p by AFF_1:26;
A11: p in Line a,p by AFF_1:26;
A12: o in Line o,p by AFF_1:26;
not B9 // Line o,p

proof

assume B9 // Line o,p ; :: thesis: contradiction
then Line a,p // Line o,p by A7, AFF_1:58;
then Line a,p = Line o,p by A10, A11, AFF_1:59;
hence contradiction by A4, A12, A10, A9, A5, AFF_1:33; :: thesis: verum

end;

then consider p9 being Element of AFP such that
A13: p9 in B9 and
A14: p9 in Line o,p by A5, A8, AFF_1:72;
A15: a,p // b,p9 by A9, A11, A6, A7, A13, AFF_1:53;
set M = Line o,a;
A16: o in Line o,a by AFF_1:26;
o <> a by A4, AFF_1:16;
then A17: Line o,a is being_line by AFF_1:def 3;
set C = Line p,x;
assume A18: 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, 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 ) ) )
then A19: Line p,x is being_line by A4, AFF_1:def 3;
then consider D being Subset of AFP such that
A20: p9 in D and
A21: Line p,x // D by AFF_1:63;
A22: p in Line p,x by AFF_1:26;
A23: LIN o,p,p9 by A12, A10, A5, A14, AFF_1:33;
A24: a in Line o,a by AFF_1:26;
A25: x in Line p,x by AFF_1:26;
A26: x in Line o,a by A18, AFF_1:def 2;
A27: not D // Line o,a

proof

assume D // Line o,a ; :: thesis: contradiction
then Line p,x // Line o,a by A21, AFF_1:58;
then Line p,x = Line o,a by A26, A25, AFF_1:59;
hence contradiction by A4, A16, A24, A22, A19, AFF_1:33; :: thesis: verum

end;

D is being_line by A21, AFF_1:50;
then consider y being Element of AFP such that
A28: y in D and
A29: y in Line o,a by A17, A27, AFF_1:72;
A30: LIN o,a,y by A16, A24, A17, A29, AFF_1:33;
p,x // p9,y by A22, A25, A20, A21, A28, 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, 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 ) ) ) by A18, A4, A23, A15, A30; :: thesis: verum

end;

now

o,a // o,b by A2, AFF_1:def 1;
then a,o // o,b by AFF_1:13;
then consider y being Element of AFP such that
A31: x,o // o,y and
A32: x,a // b,y by A1, DIRAF:47;
o,x // o,y by A31, AFF_1:13;
then A33: LIN o,x,y by AFF_1:def 1;
assume A34: 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, 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 ) ) )
a,x // b,y by A32, AFF_1:13;
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, 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 ) ) ) by A34, A33; :: 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, 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 ) ) ) by A3; :: thesis: verum