:: deftheorem DefKappa1 defines kappa_1 ROUGHIF1:def 5 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = kappa_1 R iff for x, y being Subset of R holds b₂ . (x,y) = kappa_1 (x,y) );