theorem Th3: :: TRANSLAC:3

for AFP being AffinPlane
for a, x, y being Element of AFP
for f being Permutation of the carrier of AFP st f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y holds
y = f . x