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