let AFP be AffinPlane; :: thesis: ( ( for a, b being Element of AFP 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 AFP 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 AFP; :: 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' )
assume A2: ( 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'
consider f being Permutation of the carrier of AFP such that
A3: f is translation and
A4: f . a = a' by A1;
A5: b' = f . b by A2, A3, A4, Th5;
A6: c' = f . c by A2, A3, A4, Th5;
f is dilatation by A3, TRANSGEO:def 11;
hence b,c // b',c' by A5, A6, TRANSGEO:85; :: thesis: verum

end;

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