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

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

hence
id (bool the carrier of R) cc= UAp R
by A1, ALTCAT_2:def 1; :: thesis: verum
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;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