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 Th58
.= (LAp A) /\ ((LAp A) \/ (LAp B)) by Th56
.= LAp A by XBOOLE_1:21 ;
UAp (A _/\_ (A _\/_ B)) = (UAp A) /\ (UAp (A _\/_ B)) by Th59
.= (UAp A) /\ ((UAp A) \/ (UAp B)) by Th57
.= UAp A by XBOOLE_1:21 ;
hence A _/\_ (A _\/_ B) = A by A1, Def17; :: thesis: verum