let AFP be AffinPlane; :: thesis: for a, b, x, p, q, p', q', y, x' 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,x // q,y & p',q' // x',y & p',x' // q',y & not LIN a,b,p & not LIN a,b,p' holds
x = x'
let a, b, x, p, q, p', q', y, x' 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,x // q,y & p',q' // x',y & p',x' // q',y & not LIN a,b,p & not LIN a,b,p' implies x = x' )
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,x // q,y and
A10: p',q' // x',y and
A11: p',x' // q',y and
A12: not LIN a,b,p and
A13: not LIN a,b,p' ; :: thesis: x = x'
LIN a,b,y by A2, A3, A4, A6, A8, A12, Lm10;
then A14: LIN b,a,y by AFF_1:15;
A15: b,a // q,p by A4, AFF_1:13;
A16: b,a // q',p' by A5, AFF_1:13;
A17: b,q // a,p by A6, AFF_1:13;
A18: b,q' // a,p' by A7, AFF_1:13;
A19: q,p // y,x by A8, AFF_1:13;
A20: q,y // p,x by A9, AFF_1:13;
A21: q',p' // y,x' by A10, AFF_1:13;
A22: q',y // p',x' by A11, AFF_1:13;
A23: not LIN b,a,q by A4, A6, A12, Lm5;
not LIN b,a,q' by A5, A7, A13, Lm5;
hence x = x' by A1, A2, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, Lm9; :: thesis: verum