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