theorem :: ROUGHS_5:16

for R being non empty RelStr st the InternalRel of R is total & the InternalRel of R is reflexive holds
id (bool the carrier of R) cc= f_0 R