let AFP be AffinPlane; :: thesis: for o, a, x, y, b 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 o, a, x, y, b 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:16;
set K = Line o,p;
A8: o <> p by A4, AFF_1:16;
p9 in Line o,p by A5, AFF_1:def 2;
then A9: y in Line o,p by A2, A6, A8, AFF_1:36;
assume A10: y <> o ; :: thesis: contradiction
A11: o in Line o,p by AFF_1:26;
A12: p in Line o,p by AFF_1:26;
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:26;
A15: y in Line o,a by A7, AFF_1:def 2;
A16: o in Line o,a by AFF_1:26;
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:30;
hence contradiction by A4, A13, A16, A14, AFF_1:33; :: thesis: verum