let OAS be OAffinSpace; for f being Permutation of the carrier of OAS st f is translation holds
f is positive_dilatation
let f be Permutation of the carrier of OAS; ( f is translation implies f is positive_dilatation )
assume A1:
f is translation
; f is positive_dilatation
A2:
now ( ( for x being Element of OAS holds f . x <> x ) implies f is positive_dilatation )assume A3:
for
x being
Element of
OAS holds
f . x <> x
;
f is positive_dilatation
for
a,
b being
Element of
OAS holds
a,
b // f . a,
f . b
proof
let a,
b be
Element of
OAS;
a,b // f . a,f . b
A4:
a <> f . a
by A3;
( not
a,
f . a,
b are_collinear implies
a,
b // f . a,
f . b )
by A1, Lm5;
hence
a,
b // f . a,
f . b
by A1, A4, Lm9;
verum
end; hence
f is
positive_dilatation
by Th27;
verum end;
( f = id the carrier of OAS implies f is positive_dilatation )
by Th28;
hence
f is positive_dilatation
by A1, A2; verum