theorem :: ROUGHS_5:36

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