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)

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)

proof

(A _/\_ B) _\/_ (A _/\_ C) c= A _/\_ (B _\/_ C)
let x be object ; :: 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

A2: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def 5;

consider Z, W being set such that

A3: ( Z in B & W in C & Y = Z \/ W ) by A2, SETFAM_1:def 4;

A4: ( 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 /\ (Z \/ W) in INTERSECTION (A,(UNION (B,C))) by A2, A3, SETFAM_1:def 5;

hence x in (A _/\_ B) _\/_ (A _/\_ C) by A2, A3, Th30, A4; :: thesis: verum

end;assume x in A _/\_ (B _\/_ C) ; :: thesis: x in (A _/\_ B) _\/_ (A _/\_ C)

then consider X, Y being set such that

A2: ( X in A & Y in UNION (B,C) & x = X /\ Y ) by SETFAM_1:def 5;

consider Z, W being set such that

A3: ( Z in B & W in C & Y = Z \/ W ) by A2, SETFAM_1:def 4;

A4: ( 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 /\ (Z \/ W) in INTERSECTION (A,(UNION (B,C))) by A2, A3, SETFAM_1:def 5;

hence x in (A _/\_ B) _\/_ (A _/\_ C) by A2, A3, Th30, A4; :: thesis: verum

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

A5: ( X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y ) by SETFAM_1:def 4;

A6: ( 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 UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A5, SETFAM_1:def 4;

hence x in A _/\_ (B _\/_ C) by Th30, A6; :: thesis: verum

end;assume x in (A _/\_ B) _\/_ (A _/\_ C) ; :: thesis: x in A _/\_ (B _\/_ C)

then consider X, Y being set such that

A5: ( X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y ) by SETFAM_1:def 4;

A6: ( 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 UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C))) by A5, SETFAM_1:def 4;

hence x in A _/\_ (B _\/_ C) by Th30, A6; :: thesis: verum