let U be non empty set ; :: thesis: for A, B, C being non empty IntervalSet of U holds A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
let A, B, C be non empty IntervalSet of U; :: thesis: A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
W0: A _\/_ (B _/\_ C) c= (A _\/_ B) _/\_ (A _\/_ C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A _\/_ (B _/\_ C) or x in (A _\/_ B) _/\_ (A _\/_ C) )
assume x in A _\/_ (B _/\_ C) ; :: thesis: x in (A _\/_ B) _/\_ (A _\/_ C)
then consider X, Y being set such that
W1: ( X in A & Y in INTERSECTION B,C & x = X \/ Y ) by SETFAM_1:def 4;
consider Z, W being set such that
W2: ( Z in B & W in C & Y = Z /\ W ) by SETFAM_1:def 5, W1;
ZZ: UNION A,(INTERSECTION B,C) c= INTERSECTION (UNION A,B),(UNION A,C) by Lemacik1;
X \/ (Z /\ W) in UNION A,(INTERSECTION B,C) by W1, W2, SETFAM_1:def 4;
hence x in (A _\/_ B) _/\_ (A _\/_ C) by ZZ, W1, W2; :: thesis: verum

end;

(A _\/_ B) _/\_ (A _\/_ C) c= A _\/_ (B _/\_ C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A _\/_ B) _/\_ (A _\/_ C) or x in A _\/_ (B _/\_ C) )
assume x in (A _\/_ B) _/\_ (A _\/_ C) ; :: thesis: x in A _\/_ (B _/\_ C)
then consider X, Y being set such that
E1: ( X in UNION A,B & Y in UNION A,C & x = X /\ Y ) by SETFAM_1:def 5;
P3: ( A is non empty ordered Subset-Family of & B is non empty ordered Subset-Family of & C is non empty ordered Subset-Family of ) by Nowe2;
x in INTERSECTION (UNION A,B),(UNION A,C) by SETFAM_1:def 5, E1;
hence x in A _\/_ (B _/\_ C) by Wazne1, P3; :: thesis: verum

end;

hence A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C) by W0, XBOOLE_0:def 10; :: thesis: verum