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