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