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