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 x' = (f " ) . x;
set y' = (f " ) . y;
( f . ((f " ) . x) = x & f . ((f " ) . y) = y ) by Th4;
then (f " ) . y,(f " ) . x // x,y by A1, Def7;
hence x,y // (f " ) . y,(f " ) . x by DIRAF:5; :: thesis: verum