let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} holds
(CMap (kappa R)) . (X,Y) = kappa (X,(Y `))
let X, Y be Subset of R; :: thesis: ( X <> {} implies (CMap (kappa R)) . (X,Y) = kappa (X,(Y `)) )
assume A0: X <> {} ; :: thesis: (CMap (kappa R)) . (X,Y) = kappa (X,(Y `))
(CMap (kappa R)) . (X,Y) = 1 - ((kappa R) . (X,Y)) by CDef
.= 1 - (kappa (X,Y)) by ROUGHIF1:def 2 ;
hence (CMap (kappa R)) . (X,Y) = kappa (X,(Y `)) by A0, ROUGHIF1:35; :: thesis: verum