theorem Th23: :: TRANSGEO:23

for CS being CongrSpace holds id the carrier of CS is_DIL_of CS by Lm3, Th12;