theorem Th2: :: TOPGRP_1:2

for R being 1-sorted holds (id R) /" = id R