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
A1: (id R) /" = id R by Th2;
( dom (id R) = [#] R & rng (id R) = [#] R ) by RELAT_1:71;
then (id R) .: X = ((id R) /" ) " X by TOPS_2:67;
hence (id R) " X = X by A1, FUNCT_1:162; :: thesis: verum