for R being finite Approximation_Space
for X, Y being Subset of R holds
( 0 <= (CMap (kappa R)) . (X,Y) & (CMap (kappa R)) . (X,Y) <= 1 ) by XXREAL_1:1;