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

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