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

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