let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS holds
( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b )
let f be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b )

A1: now

assume f is positive_dilatation ; :: thesis: for a, b being Element of OAS holds a,b // f . a,f . b
then f is_DIL_of OAS by Def6;
hence for a, b being Element of OAS holds a,b // f . a,f . b by Th35; :: thesis: verum

end;

now

assume for a, b being Element of OAS holds a,b // f . a,f . b ; :: thesis: f is positive_dilatation
then f is_DIL_of OAS by Th35;
hence f is positive_dilatation by Def6; :: thesis: verum

end;

hence ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b ) by A1; :: thesis: verum