theorem Th70: :: INTERVA1:70

for X being Tolerance_Space
for A being RoughSet of X holds (TRS X) _/\_ A = A by XBOOLE_1:28;