let R be finite Approximation_Space; :: thesis: 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; :: thesis: ( X \/ Y = {} implies (CMap (kappa_1 R)) . (X,Y) = 0 )
assume AA: X \/ Y = {} ; :: thesis: (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 ; :: thesis: verum