let OAS be OAffinSpace; 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; ( ( f is positive_dilatation or f is negative_dilatation ) implies f is dilatation )
assume A1:
( f is positive_dilatation or f is negative_dilatation )
; f is dilatation
now for x, y being Element of OAS holds x,y '||' f . x,f . ylet x,
y be
Element of
OAS;
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;
verum end;
hence
f is dilatation
by Th34; verum