theorem Th13: :: TRANSLAC:13

for AFP being AffinPlane
for f being Permutation of the carrier of AFP st AFP is Fanoian & f is translation & f * f = id the carrier of AFP holds
f = id the carrier of AFP