theorem Th69: :: INTERVA1:69

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