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

proof

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

end;

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