let R be finite Approximation_Space; for X, Y being Subset of R st X <> {} holds
1 - (kappa (X,Y)) = kappa (X,(Y `))
let X, Y be Subset of R; ( X <> {} implies 1 - (kappa (X,Y)) = kappa (X,(Y `)) )
assume A1:
X <> {}
; 1 - (kappa (X,Y)) = kappa (X,(Y `))
a2:
Y \/ (([#] R) \ Y) = [#] R
by XBOOLE_1:45;
kappa (X,(Y \/ (Y `))) = (kappa (X,Y)) + (kappa (X,(Y `)))
by A1, Prop1e, SUBSET_1:23;
then
(kappa (X,Y)) + (kappa (X,(Y `))) = 1
by a2, Prop1a;
hence
1 - (kappa (X,Y)) = kappa (X,(Y `))
; verum