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