let AFP be AffinPlane; :: thesis: for a, b being Element of AFP st AFP is translational holds

ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b )

let a, b be Element of AFP; :: thesis: ( AFP is translational implies ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) )

assume A1: AFP is translational ; :: thesis: ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b )

( a = b implies ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) ) by Th5;

hence ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) by A1, Lm12; :: thesis: verum

ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b )

let a, b be Element of AFP; :: thesis: ( AFP is translational implies ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) )

assume A1: AFP is translational ; :: thesis: ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b )

( a = b implies ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) ) by Th5;

hence ex f being Permutation of the carrier of AFP st

( f is translation & f . a = b ) by A1, Lm12; :: thesis: verum