let AFP be AffinPlane; :: thesis: ( ( for a, b being Element of ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b ) ) implies AFP is translational )
assume A1: for a, b being Element of ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b ) ; :: thesis: AFP is translational

now

let a, a', b, c, b', c' be Element of ; :: thesis: ( not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
consider f being Permutation of the carrier of AFP such that
A2: f is translation and
A3: f . a = a' by A1;
A4: f is dilatation by A2, TRANSGEO:def 11;
assume ( not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
then ( b' = f . b & c' = f . c ) by A2, A3, Th5;
hence b,c // b',c' by A4, TRANSGEO:85; :: thesis: verum

end;

hence AFP is translational by Th6; :: thesis: verum