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 A1: ( X = {} & Y <> {} ) ; :: thesis: (CMap (kappa_1 R)) . (X,Y) = 0
then (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y)) by PropEx3
.= 0 by A1 ;
hence (CMap (kappa_1 R)) . (X,Y) = 0 ; :: thesis: verum