let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( 0 <= ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) & ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) <= 1 )
let X, Y be Subset of R; :: thesis: ( 0 <= ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) & ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) <= 1 )
((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) = ((card (X \ Y)) / (card ([#] R))) + ((CMap (kappa_2 R)) . (Y,X)) by PropEx31
.= ((card (X \ Y)) / (card ([#] R))) + ((card (Y \ X)) / (card ([#] R))) by PropEx31
.= ((card (X \ Y)) + (card (Y \ X))) / (card ([#] R)) by XCMPLX_1:62
.= (card (X \+\ Y)) / (card ([#] R)) by CARD_2:40, XBOOLE_1:82 ;
hence ( 0 <= ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) & ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X)) <= 1 ) by NAT_1:43, XREAL_1:183; :: thesis: verum