theorem PropEx31: :: ROUGHIF2:13

for R being finite Approximation_Space
for X, Y being Subset of R holds (CMap (kappa_2 R)) . (X,Y) = (card (X \ Y)) / (card ([#] R))