theorem :: TRANSGEO:32

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is negative_dilatation holds
f " is negative_dilatation