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

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

hence
f_1 R is c=-monotone
; :: thesis: verum
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 }

hence (f_1 R) . a c= (f_1 R) . b by A2, Defff; :: thesis: verum

end;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

(f_1 R) . a = { u where u is Element of R : (UncertaintyMap R) . u meets a }
by Defff;
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;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

hence (f_1 R) . a c= (f_1 R) . b by A2, Defff; :: thesis: verum