:: deftheorem KappaDef defines kappa ROUGHIF1:def 1 :
for R being finite Approximation_Space
for X, Y being Subset of R holds
( ( X <> {} implies kappa (X,Y) = (card (X /\ Y)) / (card X) ) & ( not X <> {} implies kappa (X,Y) = 1 ) );