let R be non empty reflexive RelStr ; :: thesis: id (bool the carrier of R) cc= UAp R
set f = id (bool the carrier of R);
set g = UAp R;
A1: dom (id (bool the carrier of R)) c= dom (UAp R) by FUNCT_2:def 1;
for i being set st i in dom (id (bool the carrier of R)) holds
(id (bool the carrier of R)) . i c= (UAp R) . i

proof

let i be set ; :: thesis: ( i in dom (id (bool the carrier of R)) implies (id (bool the carrier of R)) . i c= (UAp R) . i )
assume i in dom (id (bool the carrier of R)) ; :: thesis: (id (bool the carrier of R)) . i c= (UAp R) . i
then reconsider ii = i as Subset of R ;
(UAp R) . ii = UAp ii by ROUGHS_2:def 11;
hence (id (bool the carrier of R)) . i c= (UAp R) . i by ROUGHS_2:36; :: thesis: verum

end;

hence id (bool the carrier of R) cc= UAp R by A1, ALTCAT_2:def 1; :: thesis: verum