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

proof

let a, b be Subset of R; :: thesis: ( a c= b implies (f_1 R) . a c= (f_1 R) . b )
assume A0: a c= b ; :: thesis: (f_1 R) . a c= (f_1 R) . b
A2: { u where u is Element of R : (UncertaintyMap R) . u meets a } c= { u where u is Element of R : (UncertaintyMap R) . u meets b }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { u where u is Element of R : (UncertaintyMap R) . u meets a } or t in { u where u is Element of R : (UncertaintyMap R) . u meets b } )
assume t in { u where u is Element of R : (UncertaintyMap R) . u meets a } ; :: thesis: t in { u where u is Element of R : (UncertaintyMap R) . u meets b }
then consider u being Element of R such that
B1: ( u = t & (UncertaintyMap R) . u meets a ) ;
(UncertaintyMap R) . u meets b by A0, B1, XBOOLE_1:63;
hence t in { u where u is Element of R : (UncertaintyMap R) . u meets b } by B1; :: thesis: verum

end;

(f_1 R) . a = { u where u is Element of R : (UncertaintyMap R) . u meets a } by Defff;
hence (f_1 R) . a c= (f_1 R) . b by A2, Defff; :: thesis: verum

end;

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