theorem FlipMono: :: ROUGHS_5:39
for R being non empty RelStr
for f being map of R st f is c=-monotone holds
Flip f is c=-monotone