let CS be CongrSpace; :: thesis: for f being Permutation of the carrier of CS st f is_DIL_of CS holds
f " is_DIL_of CS
let f be Permutation of the carrier of CS; :: thesis: ( f is_DIL_of CS implies f " is_DIL_of CS )
assume f is_DIL_of CS ; :: thesis: f " is_DIL_of CS
then f is_FormalIz_of the CONGR of CS by Def4;
then f " is_FormalIz_of the CONGR of CS by Lm4, Th24;
hence f " is_DIL_of CS by Def4; :: thesis: verum