theorem :: ROUGHS_5:41

for R being non empty RelStr holds Flip (f_1 R) is c=-monotone by FlipMono;