let AFP be AffinPlane; :: thesis: for a, b, o, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( 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
LIN o,a,x
let a, b, o, x, y be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( 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 LIN o,a,x )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: LIN o,a,y and
A5: ( ( 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: LIN o,a,x
assume A6: not LIN o,a,x ; :: thesis: contradiction
then A7: b <> y by A2, A3, A5, AFF_1:54;
set A = Line (o,a);
A8: Line (o,a) is being_line by A1, AFF_1:def 3;
A9: b,y // a,x by A5, A6, AFF_1:4;
A10: a in Line (o,a) by AFF_1:15;
A11: y in Line (o,a) by A4, AFF_1:def 2;
A12: o in Line (o,a) by AFF_1:15;
b in Line (o,a) by A3, AFF_1:def 2;
then Line (o,a) = Line (b,y) by A8, A7, A11, AFF_1:24;
then x in Line (o,a) by A7, A10, A9, AFF_1:22;
hence contradiction by A6, A8, A12, A10, AFF_1:21; :: thesis: verum