:: deftheorem defines positive_dilatation TRANSGEO:def 6 :
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is positive_dilatation iff f is_DIL_of OAS );