let CS be CongrSpace; :: thesis: id the carrier of CS is_DIL_of CS
id the carrier of CS is_FormalIz_of the CONGR of CS by Lm3, Th23;
hence id the carrier of CS is_DIL_of CS by Def4; :: thesis: verum