let AFP be AffinPlane; :: thesis:
let a, b, x, p, q, p', q', y, y' be Element of ; :: thesis:
assume that
A1: AFP is translational and
A2: a <> b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p',q' and
A6: a,p // b,q and
A7: a,p' // b,q' and
A8: p,q // x,y and
A9: p',q' // x,y' and
A10: p,x // q,y and
A11: p',x // q',y' and
A12: not LIN a,b,p and
A13: not LIN a,b,p' ; :: thesis:
A14: p <> q

proof

assume p = q ; :: thesis:
then p,a // p,b by A6, AFF_1:13;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A12, AFF_1:15; :: thesis:

end;

then a,b // x,y by A4, A8, AFF_1:14;
then A15: LIN a,b,y by A2, A3, AFF_1:18;
A16: not LIN p,q,x

proof

assume LIN p,q,x ; :: thesis:
then p,q // p,x by AFF_1:def 1;
then a,b // p,x by A4, A14, AFF_1:14;
then a,b // x,p by AFF_1:13;
hence contradiction by A2, A3, A12, AFF_1:18; :: thesis:

end;

A17: now

assume x = y ; :: thesis:
then x,p // x,q by A10, AFF_1:13;
then LIN x,p,q by AFF_1:def 1;
hence contradiction by A16, AFF_1:15; :: thesis:

end;

A18: p' <> q'

proof

assume p' = q' ; :: thesis:
then p',a // p',b by A7, AFF_1:13;
then LIN p',a,b by AFF_1:def 1;
hence contradiction by A13, AFF_1:15; :: thesis:

end;

A19: not LIN q,p,b

proof

A20: LIN q,p,p by AFF_1:16;
assume A21: LIN q,p,b ; :: thesis:
q,p // b,a by A4, AFF_1:13;
then LIN q,p,a by A14, A21, AFF_1:18;
hence contradiction by A12, A14, A21, A20, AFF_1:17; :: thesis:

end;

now

assume A22: LIN p,q,p' ; :: thesis:
p,q // p',q' by A2, A4, A5, AFF_1:14;
then A23: LIN p,q,q' by A14, A22, AFF_1:18;

A24: now

assume A25: for x being Element of holds
( not LIN a,p,x or x = a or x = p ) ; :: thesis:
then A26: for p, q, r being Element of st p <> q & LIN p,q,r & not r = p holds
r = q by Th2;

A27: now

assume A28: q = p' ; :: thesis:

A29: now

a,q // b,p by A4, A6, A12, A26, Th8;
then A30: q,a // p,b by AFF_1:13;
A31: q,p // a,b by A4, AFF_1:13;
assume A32: a = x ; :: thesis:
then A33: ( q,a // p,y' & not LIN q,p,a ) by A11, A14, A18, A16, A23, A25, A28, Th2, AFF_1:15;
( b = y & q,p // a,y' ) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A32, Th2;
hence y = y' by A31, A30, A33, TRANSGEO:97; :: thesis:

end;

now

A34: ( q,p // b,a & q,b // p,a ) by A4, A6, AFF_1:13;
assume A35: b = x ; :: thesis:
then A36: q,b // p,y' by A11, A14, A18, A23, A25, A28, Th2;
( a = y & q,p // b,y' ) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A35, Th2;
hence y = y' by A19, A34, A36, TRANSGEO:97; :: thesis:

end;

hence y = y' by A2, A3, A25, A29, Th2; :: thesis:

end;

now

assume A37: p = p' ; :: thesis:
then q = q' by A14, A18, A23, A25, Th2;
hence y = y' by A8, A9, A10, A11, A16, A37, TRANSGEO:97; :: thesis:

end;

hence y = y' by A14, A22, A25, A27, Th2; :: thesis:

end;

now

given p'' being Element of such that A38: LIN a,p,p'' and
A39: p'' <> a and
A40: p'' <> p ; :: thesis:
A41: not LIN p,q,p''

proof

assume LIN p,q,p'' ; :: thesis:
then A42: LIN p,p'',q by AFF_1:15;
( LIN p,p'',p & LIN p,p'',a ) by A38, AFF_1:15, AFF_1:16;
then LIN p,q,a by A40, A42, AFF_1:17;
hence contradiction by A4, A6, A12, Lm5; :: thesis:

end;

A43: not LIN p',q',p''

proof

p,q // p',q' by A2, A4, A5, AFF_1:14;
then A44: LIN p,q,q' by A14, A22, AFF_1:18;
assume LIN p',q',p'' ; :: thesis:
hence contradiction by A18, A22, A41, A44, AFF_1:20; :: thesis:

end;

consider q'' being Element of such that
A45: ( a,b // p'',q'' & a,p'' // b,q'' ) by DIRAF:47;
consider y'' being Element of such that
A46: ( p'',q'' // x,y'' & p'',x // q'',y'' ) by DIRAF:47;
A47: not LIN a,b,p''

proof

assume LIN a,b,p'' ; :: thesis:
then A48: LIN a,p'',b by AFF_1:15;
( LIN a,p'',a & LIN a,p'',p ) by A38, AFF_1:15, AFF_1:16;
hence contradiction by A12, A39, A48, AFF_1:17; :: thesis:

end;

then y = y'' by A1, A2, A3, A4, A6, A8, A10, A12, A45, A46, A41, Lm8;
hence y = y' by A1, A2, A3, A5, A7, A9, A11, A13, A45, A46, A43, A47, Lm8; :: thesis:

end;

hence y = y' by A24; :: thesis:

end;

hence y = y' by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm8; :: thesis: