let X be Tolerance_Space; :: thesis: for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A
let A, B be RoughSet of X; :: thesis: A _\/_ (A _/\_ B) = A
A1: LAp (A _\/_ (A _/\_ B)) = (LAp A) \/ (LAp (A _/\_ B))
.= (LAp A) \/ ((LAp A) /\ (LAp B))
.= LAp A by XBOOLE_1:22 ;
UAp (A _\/_ (A _/\_ B)) = (UAp A) \/ (UAp (A _/\_ B))
.= (UAp A) \/ ((UAp A) /\ (UAp B))
.= UAp A by XBOOLE_1:22 ;
hence A _\/_ (A _/\_ B) = A by A1; :: thesis: verum