let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )
let X, Y be Subset of R; :: thesis: ( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )

per cases ( X \/ Y = {} or X \/ Y <> {} ) ;

suppose X \/ Y = {} ; :: thesis: ( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )

then ( (CMap (kappa_1 R)) . (X,Y) = 0 & (CMap (kappa_1 R)) . (Y,X) = 0 ) by PropEx30;
hence ( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 ) ; :: thesis: verum

end;

suppose B1: X \/ Y <> {} ; :: thesis: ( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 )

then A1: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = ((card (X \ Y)) / (card (X \/ Y))) + ((CMap (kappa_1 R)) . (Y,X)) by PropEx3
.= ((card (X \ Y)) / (card (X \/ Y))) + ((card (Y \ X)) / (card (X \/ Y))) by PropEx3, B1
.= ((card (X \ Y)) + (card (Y \ X))) / (card (X \/ Y)) by XCMPLX_1:62
.= (card (X \+\ Y)) / (card (X \/ Y)) by CARD_2:40, XBOOLE_1:82 ;
card (X \+\ Y) <= card (X \/ Y) by Lack, NAT_1:43;
hence ( 0 <= ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) <= 1 ) by A1, XREAL_1:183; :: thesis: verum

end;

end;