let R be finite Approximation_Space; for X, Y being Subset of R st X = {} holds
(CMap (kappa R)) . (X,Y) = 0
let X, Y be Subset of R; ( X = {} implies (CMap (kappa R)) . (X,Y) = 0 )
assume A1:
X = {}
; (CMap (kappa R)) . (X,Y) = 0
G1:
kappa (X,Y) = 1
by ROUGHIF1:6, A1, XBOOLE_1:2;
(CMap (kappa R)) . (X,Y) =
1 - ((kappa R) . (X,Y))
by CDef
.=
1 - (kappa (X,Y))
by ROUGHIF1:def 2
.=
0
by G1
;
hence
(CMap (kappa R)) . (X,Y) = 0
; verum