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

let A be RoughSet of X; :: thesis: (ERS X) _\/_ A = A

thus (ERS X) _\/_ A = A ; :: thesis: verum