let AFP be AffinPlane; :: thesis: for a, b, o, x, y being Element of AFP st o <> a & 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
x = y
let a, b, o, x, y be Element of AFP; :: thesis: ( o <> a & 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 x = y )
assume that
A1: o <> a and
A2: a = b 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: x = y

A4: now :: thesis: ( LIN o,a,x & x <> o implies x = y )

A5: LIN o,x,x by AFF_1:7;
A6: LIN o,a,a by AFF_1:7;
assume that
A7: LIN o,a,x and
A8: x <> o ; :: thesis: x = y
consider p, q being Element of AFP such that
A9: not LIN o,a,p and
A10: LIN o,p,q and
A11: a,p // b,q and
A12: p,x // q,y and
A13: LIN o,a,y by A3, A7;
A14: LIN o,p,p by AFF_1:7;
A15: not LIN o,p,x

proof

assume LIN o,p,x ; :: thesis: contradiction
then A16: LIN o,x,p by AFF_1:6;
A17: LIN o,x,o by AFF_1:7;
LIN o,x,a by A7, AFF_1:6;
hence contradiction by A8, A9, A17, A16, AFF_1:8; :: thesis: verum

end;

LIN o,a,o by AFF_1:7;
then A18: LIN o,x,y by A1, A7, A13, AFF_1:8;
a,p // a,p by AFF_1:2;
then A19: p,x // p,y by A2, A9, A10, A11, A12, A6, A14, AFF_1:56;
p,x // p,x by AFF_1:2;
hence x = y by A14, A15, A18, A19, A5, AFF_1:56; :: thesis: verum

end;

now :: thesis: ( not LIN o,a,x implies x = y )

A20: LIN o,x,x by AFF_1:7;
A21: LIN o,a,a by AFF_1:7;
A22: a,x // a,x by AFF_1:2;
assume not LIN o,a,x ; :: thesis: x = y
hence x = y by A2, A3, A22, A21, A20, AFF_1:56; :: thesis: verum

end;

hence x = y by A1, A3, A4, Lm7; :: thesis: verum