let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} & Y = {} holds
(CMap (kappa_1 R)) . (X,Y) = 1
let X, Y be Subset of R; :: thesis: ( X <> {} & Y = {} implies (CMap (kappa_1 R)) . (X,Y) = 1 )
assume A1: ( X <> {} & Y = {} ) ; :: thesis: (CMap (kappa_1 R)) . (X,Y) = 1
then (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y)) by PropEx3
.= 1 by A1, XCMPLX_1:60 ;
hence (CMap (kappa_1 R)) . (X,Y) = 1 ; :: thesis: verum