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)

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

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