let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X = {} holds
(CMap (kappa R)) . (X,Y) = 0
let X, Y be Subset of R; :: thesis: ( X = {} implies (CMap (kappa R)) . (X,Y) = 0 )
assume A1: X = {} ; :: thesis: (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 ; :: thesis: verum