let R be non empty RelStr ; :: thesis:
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 : () . u meets a } c= { u where u is Element of 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 : () . u meets a } or t in { u where u is Element of R : () . u meets b } )
assume t in { u where u is Element of R : () . u meets a } ; :: thesis: t in { u where u is Element of R : () . u meets b }
then consider u being Element of R such that
B1: ( u = t & () . u meets a ) ;
(UncertaintyMap R) . u meets b by ;
hence t in { u where u is Element of R : () . u meets b } by B1; :: thesis: verum
end;
(f_1 R) . a = { u where u is Element of R : () . u meets a } by Defff;
hence (f_1 R) . a c= (f_1 R) . b by ; :: thesis: verum
end;
hence f_1 R is c=-monotone ; :: thesis: verum