let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X \/ Y <> {} holds
(CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y))
let X, Y be Subset of R; :: thesis: ( X \/ Y <> {} implies (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y)) )
assume A0: X \/ Y <> {} ; :: thesis: (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y))
A1: (CMap (kappa_1 R)) . (X,Y) = 1 - ((kappa_1 R) . (X,Y)) by CDef
.= 1 - (kappa_1 (X,Y)) by ROUGHIF1:def 5 ;
X \ Y = (X \/ Y) \ Y by XBOOLE_1:40;
then X1: card (X \ Y) = (card (X \/ Y)) - (card Y) by CARD_2:44, XBOOLE_1:7;
1 - ((card Y) / (card (X \/ Y))) = ((card (X \/ Y)) / (card (X \/ Y))) - ((card Y) / (card (X \/ Y))) by A0, XCMPLX_1:60
.= (card (X \ Y)) / (card (X \/ Y)) by X1, XCMPLX_1:120 ;
hence (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y)) by A1, A0, ROUGHIF1:def 3; :: thesis: verum