theorem :: ROUGHIF2:27

for R being finite Approximation_Space
for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds
( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )