theorem :: ROUGHS_5:40

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