let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} holds
(CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X)
let X, Y be Subset of R; :: thesis: ( X <> {} implies (CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X) )
assume A1: X <> {} ; :: thesis: (CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X)
X \ Y = X \ (X /\ Y) by XBOOLE_1:47;
then T1: card (X \ Y) = (card X) - (card (X /\ Y)) by XBOOLE_1:17, CARD_2:44;
(CMap (kappa R)) . (X,Y) = 1 - ((kappa R) . (X,Y)) by CDef
.= 1 - (kappa (X,Y)) by ROUGHIF1:def 2
.= 1 - ((card (X /\ Y)) / (card X)) by A1, ROUGHIF1:def 1
.= ((card X) / (card X)) - ((card (X /\ Y)) / (card X)) by A1, XCMPLX_1:60
.= (card (X \ Y)) / (card X) by T1, XCMPLX_1:120 ;
hence (CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X) ; :: thesis: verum