let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds (CMap (kappa_2 R)) . (X,Y) = (card (X \ Y)) / (card ([#] R))
let X, Y be Subset of R; :: thesis: (CMap (kappa_2 R)) . (X,Y) = (card (X \ Y)) / (card ([#] R))
((X `) \/ Y) ` = ((X \ Y) `) ` by SUBSET_1:14;
then A3: (card ([#] R)) - (card ((X `) \/ Y)) = card (X \ Y) by CARD_2:44;
(CMap (kappa_2 R)) . (X,Y) = 1 - ((kappa_2 R) . (X,Y)) by CDef
.= 1 - (kappa_2 (X,Y)) by ROUGHIF1:def 6
.= ((card ([#] R)) / (card ([#] R))) - ((card ((X `) \/ Y)) / (card ([#] R))) by XCMPLX_1:60
.= (card (X \ Y)) / (card ([#] R)) by A3, XCMPLX_1:120 ;
hence (CMap (kappa_2 R)) . (X,Y) = (card (X \ Y)) / (card ([#] R)) ; :: thesis: verum