let AFP be AffinPlane; :: thesis: for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
x = y
let o, a, b, x, y be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) implies x = y )
assume that
A1: ( o <> a & o <> b & LIN o,a,b ) 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ; :: thesis: x = y

A4: now

assume A5: not LIN o,a,x ; :: thesis: x = y
( a,x // a,x & LIN o,a,a & LIN o,x,x ) by AFF_1:11, AFF_1:16;
hence x = y by A2, A3, A5, AFF_1:70; :: thesis: verum

end;

now

assume A6: ( LIN o,a,x & x <> o ) ; :: thesis: x = y
then consider p, q being Element of AFP such that
A7: ( not LIN o,a,p & LIN o,p,q & a,p // b,q & p,x // q,y & LIN o,a,y ) by A3;
A8: ( a,p // a,q & a,p // a,p & LIN o,a,a & LIN o,p,p ) by A2, A7, AFF_1:11, AFF_1:16;
A9: not LIN o,p,x

proof

assume LIN o,p,x ; :: thesis: contradiction
then ( LIN o,x,o & LIN o,x,p & LIN o,x,a ) by A6, AFF_1:15, AFF_1:16;
hence contradiction by A6, A7, AFF_1:17; :: thesis: verum

end;

LIN o,a,o by AFF_1:16;
then A10: LIN o,x,y by A1, A6, A7, AFF_1:17;
( p,x // p,x & p,x // p,y & LIN o,p,p & LIN o,x,x ) by A7, A8, AFF_1:11, AFF_1:16, AFF_1:70;
hence x = y by A9, A10, AFF_1:70; :: thesis: verum

end;

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