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