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
A1: LAp (TRS X) = [#] X by MCART_1:7;
A2: UAp (TRS X) = [#] X by MCART_1:7;
A3: LAp ((TRS X) _/\_ A) = (LAp (TRS X)) /\ (LAp A) by Th58
.= LAp A by A1, XBOOLE_1:28 ;
UAp ((TRS X) _/\_ A) = (UAp (TRS X)) /\ (UAp A) by Th59
.= UAp A by A2, XBOOLE_1:28 ;
hence (TRS X) _/\_ A = A by A3, Def17; :: thesis: verum