let AFP be AffinPlane; :: thesis: for a, b, x, p, q, p', q', y, y' being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p',q' & a,p // b,q & a,p' // b,q' & p,q // x,y & p',q' // x,y' & p,x // q,y & p',x // q',y' & not LIN a,b,p & not LIN a,b,p' & not LIN p,q,p' holds
y = y'
let a, b, x, p, q, p', q', y, y' be Element of AFP; :: thesis: ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p',q' & a,p // b,q & a,p' // b,q' & p,q // x,y & p',q' // x,y' & p,x // q,y & p',x // q',y' & not LIN a,b,p & not LIN a,b,p' & not LIN p,q,p' implies y = y' )
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' and
A14: not LIN p,q,p' ; :: thesis: y = y'
A15: p,p' // q,q' by A1, A4, A5, A6, A7, A12, A13, Th6;
A16: p,q // p',q' by A2, A4, A5, AFF_1:14;
A17: p <> q

proof

assume p = q ; :: thesis: contradiction
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: verum

end;

A18: p' <> q'

proof

assume p' = q' ; :: thesis: contradiction
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: verum

end;

not LIN p,q,x

proof

assume A19: LIN p,q,x ; :: thesis: contradiction
then A20: p,q // p,x by AFF_1:def 1;
A21: x <> a by A4, A6, A12, A19, Lm5;
( p,x // a,b & a,b // a,x ) by A3, A4, A17, A20, AFF_1:14, AFF_1:def 1;
then p,x // a,x by A2, AFF_1:14;
then x,p // x,a by AFF_1:13;
then ( LIN x,p,a & LIN x,p,x & LIN a,x,b ) by A3, AFF_1:15, AFF_1:16, AFF_1:def 1;
then ( LIN x,p,a & LIN x,p,b & LIN x,p,p ) by A21, AFF_1:16, AFF_1:20;
hence contradiction by A3, A12, AFF_1:17; :: thesis: verum

end;

then A22: p',x // q',y by A1, A8, A10, A14, A15, A16, Th6;
A23: not LIN p',q',x

proof

assume A24: LIN p',q',x ; :: thesis: contradiction
then A25: p',q' // p',x by AFF_1:def 1;
A26: x <> a by A5, A7, A13, A24, Lm5;
( p',x // a,b & a,b // a,x ) by A3, A5, A18, A25, AFF_1:14, AFF_1:def 1;
then p',x // a,x by A2, AFF_1:14;
then x,p' // x,a by AFF_1:13;
then ( LIN x,p',a & LIN x,p',x & LIN a,x,b ) by A3, AFF_1:15, AFF_1:16, AFF_1:def 1;
then ( LIN x,p',a & LIN x,p',b & LIN x,p',p' ) by A26, AFF_1:16, AFF_1:20;
hence contradiction by A3, A13, AFF_1:17; :: thesis: verum

end;

p',q' // x,y by A8, A16, A17, AFF_1:14;
hence y = y' by A9, A11, A22, A23, TRANSGEO:97; :: thesis: verum