let AFP be AffinPlane; :: thesis: for a being Element of AFP ex f being Permutation of the carrier of AFP st
( f is translation & f . a = a )
let a be Element of AFP; :: thesis: ex f being Permutation of the carrier of AFP st
( f is translation & f . a = a )
take id the carrier of AFP ; :: thesis: ( id the carrier of AFP is translation & (id the carrier of AFP) . a = a )
thus ( id the carrier of AFP is translation & (id the carrier of AFP) . a = a ) by TRANSGEO:81; :: thesis: verum