let R be non empty RelStr ; :: thesis: for f being map of R st f is c=-monotone holds
Flip f is c=-monotone
let f be map of R; :: thesis: ( f is c=-monotone implies Flip f is c=-monotone )
set g = Flip f;
assume A1: f is c=-monotone ; :: thesis: Flip f is c=-monotone
for A, B being Subset of R st A c= B holds
(Flip f) . A c= (Flip f) . B

proof

let A, B be Subset of R; :: thesis: ( A c= B implies (Flip f) . A c= (Flip f) . B )
assume A c= B ; :: thesis: (Flip f) . A c= (Flip f) . B
then B ` c= A ` by SUBSET_1:12;
then f . (B `) c= f . (A `) by A1;
then (f . (A `)) ` c= (f . (B `)) ` by SUBSET_1:12;
then (Flip f) . A c= (f . (B `)) ` by ROUGHS_2:def 14;
hence (Flip f) . A c= (Flip f) . B by ROUGHS_2:def 14; :: thesis: verum

end;

hence Flip f is c=-monotone ; :: thesis: verum