for CS being CongrSpace
for f being Permutation of the carrier of CS st f is_DIL_of CS holds
f " is_DIL_of CS by Lm4, Th13;