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

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

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

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,Y) = kappa (X,(X /\ Y)) by S0, KappaDef; :: thesis: verum

end;

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

then kappa (X,Y) = 1 by KappaDef;
hence kappa (X,Y) = kappa (X,(X /\ Y)) by S1, KappaDef; :: thesis: verum

end;

end;