let X be Tolerance_Space; :: thesis: for A being RoughSet of X holds A _/\_ A = A
let A be RoughSet of X; :: thesis: A _/\_ A = A
A1: LAp (A _/\_ A) = LAp A by Th3;
UAp (A _/\_ A) = (UAp A) /\ (UAp A) by Th4;
hence A _/\_ A = A by A1, Def5; :: thesis: verum