let R be non empty RelStr ; :: thesis: f_0 R is c=-monotone
set f = f_0 R;
for a, b being Subset of R st a c= b holds
(f_0 R) . a c= (f_0 R) . b

proof

let a, b be Subset of R; :: thesis: ( a c= b implies (f_0 R) . a c= (f_0 R) . b )
assume A0: a c= b ; :: thesis: (f_0 R) . a c= (f_0 R) . b
A1: (f_0 R) . a = (UAp R) . a by UApF0
.= UAp a by ROUGHS_2:def 11 ;
(f_0 R) . b = (UAp R) . b by UApF0
.= UAp b by ROUGHS_2:def 11 ;
hence (f_0 R) . a c= (f_0 R) . b by A1, A0, ROUGHS_2:15; :: thesis: verum

end;

hence f_0 R is c=-monotone ; :: thesis: verum