let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R
for kap being RIF of R st Y c= Z holds
(CMap kap) . (X,Z) <= (CMap kap) . (X,Y)
let X, Y, Z be Subset of R; :: thesis: for kap being RIF of R st Y c= Z holds
(CMap kap) . (X,Z) <= (CMap kap) . (X,Y)
let kap be RIF of R; :: thesis: ( Y c= Z implies (CMap kap) . (X,Z) <= (CMap kap) . (X,Y) )
assume Y c= Z ; :: thesis: (CMap kap) . (X,Z) <= (CMap kap) . (X,Y)
then 1 - (kap . (X,Y)) >= 1 - (kap . (X,Z)) by XREAL_1:10, ROUGHIF1:def 8;
then (CMap kap) . (X,Y) >= 1 - (kap . (X,Z)) by CDef;
hence (CMap kap) . (X,Z) <= (CMap kap) . (X,Y) by CDef; :: thesis: verum