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 Th1;
s: ((LAp A) \/ (LAp B)) \/ (LAp C) = (LAp A) \/ ((LAp B) \/ (LAp C)) by XBOOLE_1:4;
d: (LAp A) \/ ((LAp B) \/ (LAp C)) = (LAp A) \/ (LAp (B _\/_ C)) by Th1;
(LAp A) \/ (LAp (B _\/_ C)) = LAp (A _\/_ (B _\/_ C)) by Th1;
then T1: LAp ((A _\/_ B) _\/_ C) = LAp (A _\/_ (B _\/_ C)) by Th1, a, s, d;
A2: UAp ((A _\/_ B) _\/_ C) = (UAp (A _\/_ B)) \/ (UAp C) by Th2;
q: (UAp (A _\/_ B)) \/ (UAp C) = ((UAp A) \/ (UAp B)) \/ (UAp C) by Th2;
w: ((UAp A) \/ (UAp B)) \/ (UAp C) = (UAp A) \/ ((UAp B) \/ (UAp C)) by XBOOLE_1:4;
e: (UAp A) \/ ((UAp B) \/ (UAp C)) = (UAp A) \/ (UAp (B _\/_ C)) by Th2;
(UAp A) \/ (UAp (B _\/_ C)) = UAp (A _\/_ (B _\/_ C)) by Th2;
hence (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by T1, Def5, A2, q, w, e; :: thesis: verum