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