:: deftheorem defines dilatation TRANSGEO:def 8 :
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is dilatation iff f is_FormalIz_of lambda the CONGR of OAS );