theorem Th2: :: TOPGRP_1:2
for R being 1-sorted holds (id R) /" = id R