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:4;

A4: LAp ((A _\/_ B) _\/_ C) = LAp (A _\/_ (B _\/_ C)) by A2;

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

thus (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by A4, A7; :: 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:4;

A4: LAp ((A _\/_ B) _\/_ C) = LAp (A _\/_ (B _\/_ C)) by A2;

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

thus (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C) by A4, A7; :: thesis: verum