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 <> 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;

A16: not LIN p,q,x

proof

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

end;

A22: p,q // p',q' by A2, A4, A5, AFF_1:14;
then A23: p',q' // x,y by A8, A15, AFF_1:14;
A24: 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;

A25: not LIN p',q',x

proof

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

end;

p,p' // q,q' by A1, A4, A5, A6, A7, A12, A13, Th6;
then p',x // q',y by A1, A8, A10, A14, A22, A16, Th6;
hence y = y' by A9, A11, A25, A23, TRANSGEO:97; :: thesis: verum