let X be Tolerance_Space; :: thesis: for A being RoughSet of X holds (TRS X) _/\_ A = A
let A be RoughSet of X; :: thesis: (TRS X) _/\_ A = A
A3: LAp ((TRS X) _/\_ A) = (LAp (TRS X)) /\ (LAp A)
.= LAp A by XBOOLE_1:28 ;
UAp ((TRS X) _/\_ A) = (UAp (TRS X)) /\ (UAp A)
.= UAp A by XBOOLE_1:28 ;
hence (TRS X) _/\_ A = A by A3; :: thesis: verum