theorem :: ROUGHS_5:4
for R being non empty RelStr
for f being map of R
for x, y being Subset of R holds Flip (Flip f) = f by ROUGHS_2:23;