theorem :: TOPGRP_1:3

for R being 1-sorted
for X being Subset of R holds (id R) " X = X