theorem :: ROUGHIF1:32

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y)) & kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y))) ) by Lemma4f1, Lemma4f2;