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