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)

A2: ((LAp A) /\ (LAp B)) /\ (LAp C) = (LAp A) /\ ((LAp B) /\ (LAp C)) by XBOOLE_1:16;

((UAp A) /\ (UAp B)) /\ (UAp C) = (UAp A) /\ ((UAp B) /\ (UAp C)) by XBOOLE_1:16;

hence (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C) by A2; :: thesis: verum

let A, B, C be RoughSet of X; :: thesis: (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)

A2: ((LAp A) /\ (LAp B)) /\ (LAp C) = (LAp A) /\ ((LAp B) /\ (LAp C)) by XBOOLE_1:16;

((UAp A) /\ (UAp B)) /\ (UAp C) = (UAp A) /\ ((UAp B) /\ (UAp C)) by XBOOLE_1:16;

hence (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C) by A2; :: thesis: verum