let R be finite Approximation_Space; :: thesis: for X, Z, W being Subset of R st X <> {} & Z \/ W = [#] R & Z misses W holds
(kappa (X,Z)) + (kappa (X,W)) = 1
let X, Z, W be Subset of R; :: thesis: ( X <> {} & Z \/ W = [#] R & Z misses W implies (kappa (X,Z)) + (kappa (X,W)) = 1 )
assume A1: ( X <> {} & Z \/ W = [#] R & Z misses W ) ; :: thesis: (kappa (X,Z)) + (kappa (X,W)) = 1
A3: kappa (X,W) = (card (X /\ W)) / (card X) by A1, KappaDef;
A6: X = X /\ (Z \/ W) by A1
.= (X /\ Z) \/ (X /\ W) by XBOOLE_1:23 ;
A4: (card (X /\ Z)) + (card (X /\ W)) = card X by A6, A1, CARD_2:40, XBOOLE_1:76;
(kappa (X,Z)) + (kappa (X,W)) = ((card (X /\ Z)) / (card X)) + ((card (X /\ W)) / (card X)) by A1, A3, KappaDef
.= (card X) / (card X) by A4, XCMPLX_1:62 ;
hence (kappa (X,Z)) + (kappa (X,W)) = 1 by XCMPLX_1:60, A1; :: thesis: verum