let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))
let X, Y be Subset of R; :: thesis: kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))
per cases ( X \/ (X /\ Y) <> {} or X \/ (X /\ Y) = {} ) ;
suppose S0: X \/ (X /\ Y) <> {} ; :: thesis: kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))
then S2: X <> {} ;
S3: kappa_1 (X,(X /\ Y)) = (card (X /\ Y)) / (card (X \/ (X /\ Y))) by Kappa1, S0
.= (card (X /\ Y)) / (card X) by XBOOLE_1:22 ;
(X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51;
hence kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) by S3, S2, Kappa1; :: thesis: verum
end;
suppose S0: X \/ (X /\ Y) = {} ; :: thesis: kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))
then S4: kappa_1 (X,(X /\ Y)) = 1 by Kappa1;
(X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51
.= X \/ (X /\ Y) by XBOOLE_1:22 ;
hence kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) by S4, S0, Kappa1; :: thesis: verum
end;
end;