theorem :: ROUGHS_5:17

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