let OAS be OAffinSpace; :: thesis: 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; :: thesis: ( f is translation implies f is positive_dilatation )
assume A1: f is translation ; :: thesis: f is positive_dilatation

A2: now :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence f is positive_dilatation by Th27; :: thesis: verum

end;

( f = id the carrier of OAS implies f is positive_dilatation ) by Th28;
hence f is positive_dilatation by A1, A2; :: thesis: verum