let R be non empty RelStr ; :: thesis: ( the InternalRel of R is total & the InternalRel of R is reflexive implies id (bool the carrier of R) cc= f_0 R )
assume zz: ( the InternalRel of R is total & the InternalRel of R is reflexive ) ; :: thesis: id (bool the carrier of R) cc= f_0 R
set f = id (bool the carrier of R);
set g = f_0 R;
A1: dom (id (bool the carrier of R)) c= dom (f_0 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= (f_0 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= (f_0 R) . i )
assume k2: i in dom (id (bool the carrier of R)) ; :: thesis: (id (bool the carrier of R)) . i c= (f_0 R) . i
then reconsider ii = i as Subset of R ;
i c= { u where u is Element of R : (tau R) . u meets ii }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in i or y in { u where u is Element of R : (tau R) . u meets ii } )
assume D1: y in i ; :: thesis: y in { u where u is Element of R : (tau R) . u meets ii }
then reconsider wy = y as Element of R by k2;
[wy,wy] in the InternalRel of R by zz, LATTAD_1:1;
then wy in (tau R) . wy by For3A;
then (tau R) . wy meets ii by XBOOLE_0:3, D1;
hence y in { u where u is Element of R : (tau R) . u meets ii } ; :: thesis: verum

end;

hence (id (bool the carrier of R)) . i c= (f_0 R) . i by Defff; :: thesis: verum

end;

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