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