let X be Tolerance_Space; :: thesis: for A being RoughSet of X holds (ERS X) _\/_ A = A
let A be RoughSet of X; :: thesis: (ERS X) _\/_ A = A
thus (ERS X) _\/_ A = A ; :: thesis: verum