let AFP be AffinPlane; :: thesis: for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & ( ( 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 ) ) ) holds
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
let o, a, b, x, y be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b & ( ( 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 ) ) ) implies ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: ( ( 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 ) ) ) ; :: thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
A5: LIN o,b,a by A3, AFF_1:15;

A6: now

assume A7: LIN o,a,x ; :: thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
then consider p, q being Element of AFP such that
A8: not LIN o,a,p and
A9: LIN o,p,q and
A10: a,p // b,q and
A11: p,x // q,y and
A12: LIN o,a,y by A4;
A13: not LIN o,p,a by A8, AFF_1:15;
A14: q,y // p,x by A11, AFF_1:13;
A15: b,q // a,p by A10, AFF_1:13;
A16: LIN o,q,p by A9, AFF_1:15;
LIN o,a,o by AFF_1:16;
then A17: LIN o,b,x by A1, A3, A7, AFF_1:17;
set A = Line (o,b);
A18: o in Line (o,b) by AFF_1:26;
A19: a in Line (o,b) by A5, AFF_1:def 2;
A20: Line (o,b) is being_line by A2, AFF_1:def 3;
p,a // q,b by A10, AFF_1:13;
then A21: q <> o by A2, A3, A13, AFF_1:69;
A22: not LIN o,b,q

proof

assume LIN o,b,q ; :: thesis: contradiction
then q in Line (o,b) by AFF_1:def 2;
then p in Line (o,b) by A21, A20, A18, A16, AFF_1:39;
hence contradiction by A8, A20, A18, A19, AFF_1:33; :: thesis: verum

end;

y in Line (o,b) by A1, A12, A20, A18, A19, AFF_1:39;
hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A15, A14, A16, A22, A17, AFF_1:15, AFF_1:def 2; :: thesis: verum

end;

now

assume A23: not LIN o,a,x ; :: thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
then A24: not LIN o,a,y by A1, A2, A3, A4, Lm5;
not LIN o,b,y

proof

A25: LIN o,b,o by AFF_1:16;
assume A26: LIN o,b,y ; :: thesis: contradiction
LIN o,b,a by A3, AFF_1:15;
hence contradiction by A2, A24, A26, A25, AFF_1:17; :: thesis: verum

end;

hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A4, A23, AFF_1:13, AFF_1:15; :: thesis: verum

end;

hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A6; :: thesis: verum