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

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

A3: (LAp A) /\ ((LAp B) \/ (LAp C)) = ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) by XBOOLE_1:23;

A5: LAp (A _/\_ (B _\/_ C)) = LAp ((A _/\_ B) _\/_ (A _/\_ C)) by A3;

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

UAp (A _/\_ (B _\/_ C)) = UAp ((A _/\_ B) _\/_ (A _/\_ C)) by A8;

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

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

A3: (LAp A) /\ ((LAp B) \/ (LAp C)) = ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) by XBOOLE_1:23;

A5: LAp (A _/\_ (B _\/_ C)) = LAp ((A _/\_ B) _\/_ (A _/\_ C)) by A3;

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

UAp (A _/\_ (B _\/_ C)) = UAp ((A _/\_ B) _\/_ (A _/\_ C)) by A8;

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