theorem :: ROUGHIF2:34
for R being finite Approximation_Space
for X, Y, Z being Subset of R holds ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z)