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 :: thesis: for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, a9, b, c, b9, c9 be Element of AFP; :: thesis: ( not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
consider f being Permutation of the carrier of AFP such that
A2: f is translation and
A3: f . a = a9 by A1;
A4: f is dilatation by A2, TRANSGEO:def 11;
assume ( not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 ) ; :: thesis: b,c // b9,c9
then ( b9 = f . b & c9 = f . c ) by A2, A3, Th3;
hence b,c // b9,c9 by A4, TRANSGEO:68; :: thesis: verum
end;
hence AFP is translational by Th4; :: thesis: verum