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

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

hence
Flip f is c=-monotone
; :: thesis: verum
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;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