let AFP be AffinPlane; :: thesis: for o, a, b, y, x 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 o, a, b, y, x 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:68;
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:13;
A10: a in Line o,a by AFF_1:26;
A11: y in Line o,a by A4, AFF_1:def 2;
A12: o in Line o,a by AFF_1:26;
b in Line o,a by A3, AFF_1:def 2;
then Line o,a = Line b,y by A8, A7, A11, AFF_1:38;
then x in Line o,a by A7, A10, A9, AFF_1:36;
hence contradiction by A6, A8, A12, A10, AFF_1:33; :: thesis: verum