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