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
A1: LAp (ERS X) = {} by MCART_1:7;
A2: UAp (ERS X) = {} by MCART_1:7;
A3: LAp ((ERS X) _\/_ A) = LAp A by A1, Th56;
UAp ((ERS X) _\/_ A) = UAp A by A2, Th57;
hence (ERS X) _\/_ A = A by A3, Def17; :: thesis: verum