let X be Tolerance_Space; :: thesis: for A being RoughSet of X holds A _\/_ A = A
let A be RoughSet of X; :: thesis: A _\/_ A = A
A1: LAp (A _\/_ A) = LAp A by Th56;
UAp (A _\/_ A) = (UAp A) \/ (UAp A) by Th57;
hence A _\/_ A = A by A1, Def17; :: thesis: verum