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:13;
set K = Line (o,p);
o <> p by A4, AFF_1:7;
then A5: Line (o,p) is being_line by AFF_1:def 3;
set A = Line (a,p);
a <> p by A4, AFF_1:7;
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:49;
A8: B9 is being_line by A7, AFF_1:36;
A9: a in Line (a,p) by AFF_1:15;
A10: p in Line (o,p) by AFF_1:15;
A11: p in Line (a,p) by AFF_1:15;
A12: o in Line (o,p) by AFF_1:15;
not B9 // Line (o,p)

proof

assume B9 // Line (o,p) ; :: thesis: contradiction
then Line (a,p) // Line (o,p) by A7, AFF_1:44;
then Line (a,p) = Line (o,p) by A10, A11, AFF_1:45;
hence contradiction by A4, A12, A10, A9, A5, AFF_1:21; :: 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:58;
A15: a,p // b,p9 by A9, A11, A6, A7, A13, AFF_1:39;
set M = Line (o,a);
A16: o in Line (o,a) by AFF_1:15;
o <> a by A4, AFF_1:7;
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:49;
A22: p in Line (p,x) by AFF_1:15;
A23: LIN o,p,p9 by A12, A10, A5, A14, AFF_1:21;
A24: a in Line (o,a) by AFF_1:15;
A25: x in Line (p,x) by AFF_1:15;
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:44;
then Line (p,x) = Line (o,a) by A26, A25, AFF_1:45;
hence contradiction by A4, A16, A24, A22, A19, AFF_1:21; :: thesis: verum

end;

D is being_line by A21, AFF_1:36;
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:58;
A30: LIN o,a,y by A16, A24, A17, A29, AFF_1:21;
p,x // p9,y by A22, A25, A20, A21, A28, AFF_1:39;
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:4;
then consider y being Element of AFP such that
A31: x,o // o,y and
A32: x,a // b,y by A1, DIRAF:40;
o,x // o,y by A31, AFF_1:4;
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:4;
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