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)
P0: 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
P1: ( X in A & Y in UNION B,C & x = X /\ Y ) by SETFAM_1:def 5;
consider Z, W being set such that
P2: ( Z in B & W in C & Y = Z \/ W ) by SETFAM_1:def 4, P1;
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 /\ (Z \/ W) in INTERSECTION A,(UNION B,C) by SETFAM_1:def 5, P1, P2;
hence x in (A _/\_ B) _\/_ (A _/\_ C) by P1, P2, Wazne2, P3; :: 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
K1: ( X in INTERSECTION A,B & Y in INTERSECTION A,C & x = X \/ Y ) by SETFAM_1:def 4;
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 UNION (INTERSECTION A,B),(INTERSECTION A,C) by SETFAM_1:def 4, K1;
hence x in A _/\_ (B _\/_ C) by Wazne2, P3; :: thesis: verum

end;

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