:: deftheorem Delta1 defines delta_1 ROUGHIF2:def 4 :
for R being finite Approximation_Space
for b₂ being preRIF of R holds
( b₂ = delta_1 R iff for x, y being Subset of R holds b₂ . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) );