for X being Tolerance_Space
for A being RoughSet of X holds (ERS X) _\/_ A = A ;