theorem :: ROUGHS_5:18

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_1 R