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