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)) by Th1
.= (LAp A) \/ ((LAp A) /\ (LAp B)) by Th3
.= LAp A by XBOOLE_1:22 ;
UAp (A _\/_ (A _/\_ B)) = (UAp A) \/ (UAp (A _/\_ B)) by Th2
.= (UAp A) \/ ((UAp A) /\ (UAp B)) by Th4
.= UAp A by XBOOLE_1:22 ;
hence A _\/_ (A _/\_ B) = A by A1, Def5; :: thesis: verum