let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is positive_dilatation holds
f " is positive_dilatation
let f be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation implies f " is positive_dilatation )
assume A1: f is positive_dilatation ; :: thesis: f " is positive_dilatation
A2: OAS is CongrSpace by Th40;
f is_DIL_of OAS by A1, Def6;
then f " is_DIL_of OAS by A2, Th38;
hence f " is positive_dilatation by Def6; :: thesis: verum