let AFP be AffinPlane; :: thesis: for a, b, p, p9, q, q9, x, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 holds
y = y9
let a, b, p, p9, q, q9, x, y, y9 be Element of AFP; :: thesis: ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 implies y = y9 )
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 // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9 and
A14: not LIN p,q,p9 ; :: thesis: y = y9
A15: p <> q
proof
assume p = q ; :: thesis: contradiction
then p,a // p,b by A6, AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A12, AFF_1:6; :: 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:5;
a,b // a,x by A3, AFF_1:def 1;
then p,x // a,x by A2, A18, AFF_1:5;
then x,p // x,a by AFF_1:4;
then A19: LIN x,p,a by AFF_1:def 1;
A20: ( LIN x,p,x & LIN a,x,b ) by A3, AFF_1:6, AFF_1:7;
A21: LIN x,p,p by AFF_1:7;
x <> a by A4, A6, A12, A17, Lm5;
then LIN x,p,b by A19, A20, AFF_1:11;
hence contradiction by A3, A12, A19, A21, AFF_1:8; :: thesis: verum
end;
A22: p,q // p9,q9 by A2, A4, A5, AFF_1:5;
then A23: p9,q9 // x,y by A8, A15, AFF_1:5;
A24: p9 <> q9
proof
assume p9 = q9 ; :: thesis: contradiction
then p9,a // p9,b by A7, AFF_1:4;
then LIN p9,a,b by AFF_1:def 1;
hence contradiction by A13, AFF_1:6; :: thesis: verum
end;
A25: not LIN p9,q9,x
proof
assume A26: LIN p9,q9,x ; :: thesis: contradiction
then p9,q9 // p9,x by AFF_1:def 1;
then A27: p9,x // a,b by A5, A24, AFF_1:5;
a,b // a,x by A3, AFF_1:def 1;
then p9,x // a,x by A2, A27, AFF_1:5;
then x,p9 // x,a by AFF_1:4;
then A28: LIN x,p9,a by AFF_1:def 1;
A29: ( LIN x,p9,x & LIN a,x,b ) by A3, AFF_1:6, AFF_1:7;
A30: LIN x,p9,p9 by AFF_1:7;
x <> a by A5, A7, A13, A26, Lm5;
then LIN x,p9,b by A28, A29, AFF_1:11;
hence contradiction by A3, A13, A28, A30, AFF_1:8; :: thesis: verum
end;
p,p9 // q,q9 by A1, A4, A5, A6, A7, A12, A13, Th4;
then p9,x // q9,y by A1, A8, A10, A14, A22, A16, Th4;
hence y = y9 by A9, A11, A25, A23, TRANSGEO:80; :: thesis: verum