theorem PropEx3k: :: ROUGHIF2:8

for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
(CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X)