let R be 1-sorted ; :: thesis: for X being Subset of R holds (id R) " X = X
let X be Subset of R; :: thesis: (id R) " X = X
rng (id R) = [#] R by RELAT_1:71;
then A1: (id R) .: X = ((id R) /") " X by TOPS_2:67;
(id R) /" = id R by Th2;
hence (id R) " X = X by A1, FUNCT_1:162; :: thesis: verum