let R be finite Approximation_Space; 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; ( X <> {} implies (CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X) )
assume A1:
X <> {}
; (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)
; verum