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:45;
then A1: (id R) .: X = ((id R) /") " X by TOPS_2:54;
(id R) /" = id R by Th2;
hence (id R) " X = X by A1, FUNCT_1:92; :: thesis: verum