let AFP be AffinPlane; ( ( 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 )
; AFP is translational
now 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,c9let a,
a9,
b,
c,
b9,
c9 be
Element of
AFP;
( 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 )
;
b,c // b9,c9then
(
b9 = f . b &
c9 = f . c )
by A2, A3, Th3;
hence
b,
c // b9,
c9
by A4, TRANSGEO:68;
verum end;
hence
AFP is translational
by Th4; verum