let R be finite Approximation_Space; for X, Y being Subset of R st X \/ Y = {} holds
(CMap (kappa_1 R)) . (X,Y) = 0
let X, Y be Subset of R; ( X \/ Y = {} implies (CMap (kappa_1 R)) . (X,Y) = 0 )
assume AA:
X \/ Y = {}
; (CMap (kappa_1 R)) . (X,Y) = 0
A1: (kappa_1 R) . (X,Y) =
kappa_1 (X,Y)
by ROUGHIF1:def 5
.=
1
by AA, ROUGHIF1:def 3
;
(CMap (kappa_1 R)) . (X,Y) =
1 - ((kappa_1 R) . (X,Y))
by CDef
.=
0
by A1
;
hence
(CMap (kappa_1 R)) . (X,Y) = 0
; verum