let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is negative_dilatation holds
f " is negative_dilatation
let f be Permutation of the carrier of OAS; :: thesis: ( f is negative_dilatation implies f " is negative_dilatation )
assume A1: f is negative_dilatation ; :: thesis: f " is negative_dilatation
let x be Element of OAS; :: according to TRANSGEO:def 7 :: thesis: for b being Element of OAS holds x,b // (f ") . b,(f ") . x
let y be Element of OAS; :: thesis: x,y // (f ") . y,(f ") . x
set x9 = (f ") . x;
set y9 = (f ") . y;
( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2;
then (f ") . y,(f ") . x // x,y by A1;
hence x,y // (f ") . y,(f ") . x by DIRAF:2; :: thesis: verum