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

hence f is positive_dilatation by A1, A2; :: thesis: verum

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 )

( f = id the carrier of OAS implies f is positive_dilatation )
by Th28;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

end;for a, b being Element of OAS holds a,b // f . a,f . b

proof

hence
f is positive_dilatation
by Th27; :: thesis: verum
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;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

hence f is positive_dilatation by A1, A2; :: thesis: verum