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) by Lemacik1;
(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 U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U ) 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