let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds
((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1
let X, Y be Subset of R; :: thesis: ( ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) implies ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1 )
assume ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) ; :: thesis: ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1

per cases then ( ( X = {} & Y <> {} ) or ( Y = {} & X <> {} ) ) ;

suppose A0: ( X = {} & Y <> {} ) ; :: thesis: ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1

then ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 0 + ((CMap (kappa R)) . (Y,X)) by PropEx3k0
.= (card (Y \ X)) / (card Y) by A0, PropEx3k
.= (card Y) / (card Y) by A0 ;
hence ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1 by A0, XCMPLX_1:60; :: thesis: verum

end;

suppose A0: ( Y = {} & X <> {} ) ; :: thesis: ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1

then ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((card (X \ Y)) / (card (X \/ Y))) + ((CMap (kappa R)) . (Y,X)) by PropEx3k
.= ((card (X \ Y)) / (card (X \/ Y))) + 0 by PropEx3k0, A0
.= (card X) / (card X) by A0 ;
hence ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1 by A0, XCMPLX_1:60; :: thesis: verum

end;

end;