theorem :: ROUGHIF2:16
for R being finite Approximation_Space
for X, Y being Subset of R holds
( (CMap (kappa R)) . (X,Y) = 0 iff X c= Y )