let X be Tolerance_Space; :: thesis: for A, B, C being RoughSet of X holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
let A, B, C be RoughSet of X; :: thesis: (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
a: (LAp (A _/\_ B)) /\ (LAp C) = ((LAp A) /\ (LAp B)) /\ (LAp C) by Th3;
s: ((LAp A) /\ (LAp B)) /\ (LAp C) = (LAp A) /\ ((LAp B) /\ (LAp C)) by XBOOLE_1:16;
q: (UAp (A _/\_ B)) /\ (UAp C) = ((UAp A) /\ (UAp B)) /\ (UAp C) by Th4;
w: ((UAp A) /\ (UAp B)) /\ (UAp C) = (UAp A) /\ ((UAp B) /\ (UAp C)) by XBOOLE_1:16;
(UAp A) /\ ((UAp B) /\ (UAp C)) = (UAp A) /\ (UAp (B _/\_ C)) by Th4;
hence (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C) by a, s, Th3, q, w; :: thesis: verum