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)
A1: A _\/_ (B _/\_ C) c= (A _\/_ B) _/\_ (A _\/_ C) by Lm1;
(A _\/_ B) _/\_ (A _\/_ C) c= A _\/_ (B _/\_ C)

proof

let x be object ; :: 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
A2: ( X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y ) by SETFAM_1:def 5;
A3: ( 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 Lm4;
x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) by A2, SETFAM_1:def 5;
hence x in A _\/_ (B _/\_ C) by Th29, A3; :: thesis: verum

end;

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