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)
A0: LAp (A _/\_ (B _\/_ C)) = (LAp A) /\ (LAp (B _\/_ C)) by Th3;
A1: (LAp A) /\ (LAp (B _\/_ C)) = (LAp A) /\ ((LAp B) \/ (LAp C)) by Th1;
A2: (LAp A) /\ ((LAp B) \/ (LAp C)) = ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) by XBOOLE_1:23;
A3: ((LAp A) /\ (LAp B)) \/ ((LAp A) /\ (LAp C)) = (LAp (A _/\_ B)) \/ ((LAp A) /\ (LAp C)) by Th3;
(LAp (A _/\_ B)) \/ ((LAp A) /\ (LAp C)) = (LAp (A _/\_ B)) \/ (LAp (A _/\_ C)) by Th3;
then T1: LAp (A _/\_ (B _\/_ C)) = LAp ((A _/\_ B) _\/_ (A _/\_ C)) by A0, A1, A2, A3, Th1;
B0: UAp (A _/\_ (B _\/_ C)) = (UAp A) /\ (UAp (B _\/_ C)) by Th4;
B1: (UAp A) /\ (UAp (B _\/_ C)) = (UAp A) /\ ((UAp B) \/ (UAp C)) by Th2;
B2: (UAp A) /\ ((UAp B) \/ (UAp C)) = ((UAp A) /\ (UAp B)) \/ ((UAp A) /\ (UAp C)) by XBOOLE_1:23;
B3: ((UAp A) /\ (UAp B)) \/ ((UAp A) /\ (UAp C)) = (UAp (A _/\_ B)) \/ ((UAp A) /\ (UAp C)) by Th4;
(UAp (A _/\_ B)) \/ ((UAp A) /\ (UAp C)) = (UAp (A _/\_ B)) \/ (UAp (A _/\_ C)) by Th4;
then UAp (A _/\_ (B _\/_ C)) = UAp ((A _/\_ B) _\/_ (A _/\_ C)) by B0, B1, B2, B3, Th2;
hence A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C) by T1, Def5; :: thesis: verum