let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))
let X, Y be Subset of R; :: thesis: kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

per cases ( X \/ (X /\ Y) <> {} or X \/ (X /\ Y) = {} ) ;

suppose S0: X \/ (X /\ Y) <> {} ; :: thesis: kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

then S3: kappa_1 (X,(X /\ Y)) = (card (X /\ Y)) / (card (X \/ (X /\ Y))) by Kappa1
.= (card (X /\ Y)) / (card X) by XBOOLE_1:22 ;
X <> {} by S0;
then kappa (X,(X /\ Y)) = (card (X /\ (X /\ Y))) / (card X) by KappaDef
.= (card ((X /\ X) /\ Y)) / (card X) by XBOOLE_1:16 ;
hence kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) by S3; :: thesis: verum

end;

suppose S0: X \/ (X /\ Y) = {} ; :: thesis: kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

then S3: kappa_1 (X,(X /\ Y)) = 1 by Kappa1;
X = {} by S0;
hence kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) by S3, KappaDef; :: thesis: verum

end;

end;