let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds

f is dilatation

let f be Permutation of the carrier of OAS; :: thesis: ( ( f is positive_dilatation or f is negative_dilatation ) implies f is dilatation )

assume A1: ( f is positive_dilatation or f is negative_dilatation ) ; :: thesis: f is dilatation

f is dilatation

let f be Permutation of the carrier of OAS; :: thesis: ( ( f is positive_dilatation or f is negative_dilatation ) implies f is dilatation )

assume A1: ( f is positive_dilatation or f is negative_dilatation ) ; :: thesis: f is dilatation

now :: thesis: for x, y being Element of OAS holds x,y '||' f . x,f . y

hence
f is dilatation
by Th34; :: thesis: verumlet x, y be Element of OAS; :: thesis: x,y '||' f . x,f . y

( x,y // f . x,f . y or x,y // f . y,f . x ) by A1, Th27;

hence x,y '||' f . x,f . y by DIRAF:def 4; :: thesis: verum

end;( x,y // f . x,f . y or x,y // f . y,f . x ) by A1, Th27;

hence x,y '||' f . x,f . y by DIRAF:def 4; :: thesis: verum