theorem :: ROUGHIF1:33
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = kappa (X,(X /\ Y)) & kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) & kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) ) by LemmaKap1, LemmaKap2, LemmaKap3;