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 Th58;
UAp (A _/\_ A) = (UAp A) /\ (UAp A) by Th59;
hence A _/\_ A = A by A1, Def17; :: thesis: verum