:: deftheorem defines is_DIL_of TRANSGEO:def 4 :
for AS being non empty AffinStruct
for f being Permutation of the carrier of AS holds
( f is_DIL_of AS iff f is_FormalIz_of the CONGR of AS );