theorem Prop6e1: :: ROUGHIF2:25

for R being finite Approximation_Space
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 )