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
A0: LAp (ERS X) = {} by MCART_1:7;
A2: UAp (ERS X) = {} by MCART_1:7;
A1: LAp ((ERS X) _\/_ A) = LAp A by A0, Th1;
UAp ((ERS X) _\/_ A) = UAp A by A2, Th2;
hence (ERS X) _\/_ A = A by A1, Def5; :: thesis: verum