theorem Prop4b: :: ROUGHIF1:15

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )