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)
A1: (LAp (A _\/_ B)) \/ (LAp C) = ((LAp A) \/ (LAp B)) \/ (LAp C) by Th56;
A2: ((LAp A) \/ (LAp B)) \/ (LAp C) = (LAp A) \/ ((LAp B) \/ (LAp C)) by XBOOLE_1:4;
A3: (LAp A) \/ ((LAp B) \/ (LAp C)) = (LAp A) \/ (LAp (B _\/_ C)) by Th56;
(LAp A) \/ (LAp (B _\/_ C)) = LAp (A _\/_ (B _\/_ C)) by Th56;
then A4: LAp ((A _\/_ B) _\/_ C) = LAp (A _\/_ (B _\/_ C)) by Th56, A1, A2, A3;
A5: UAp ((A _\/_ B) _\/_ C) = (UAp (A _\/_ B)) \/ (UAp C) by Th57;
A6: (UAp (A _\/_ B)) \/ (UAp C) = ((UAp A) \/ (UAp B)) \/ (UAp C) by Th57;
A7: ((UAp A) \/ (UAp B)) \/ (UAp C) = (UAp A) \/ ((UAp B) \/ (UAp C)) by XBOOLE_1:4;
A8: (UAp A) \/ ((UAp B) \/ (UAp C)) = (UAp A) \/ (UAp (B _\/_ C)) by Th57;
(UAp A) \/ (UAp (B _\/_ C)) = UAp (A _\/_ (B _\/_ C)) by Th57;
hence (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by A4, Def17, A5, A6, A7, A8; :: thesis: verum