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