theorem :: ROUGHIF2:14

for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
( kappa (X,Y) = ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) & ((CMap (kappa_1 R)) . (X,(Y `))) / (kappa_1 ((Y `),X)) = ((CMap (kappa_2 R)) . (X,(Y `))) / (kappa_2 (([#] R),X)) )