let U be non empty set ; :: thesis: for A, B, C being non empty IntervalSet of U holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
let A, B, C be non empty IntervalSet of U; :: thesis: (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)
A1: (A _\/_ B) _\/_ C c= A _\/_ (B _\/_ C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A _\/_ B) _\/_ C or x in A _\/_ (B _\/_ C) )
assume x in (A _\/_ B) _\/_ C ; :: thesis: x in A _\/_ (B _\/_ C)
then consider X, Y being set such that
A3: ( X in UNION A,B & Y in C & x = X \/ Y ) by SETFAM_1:def 4;
consider Z, W being set such that
A4: ( Z in A & W in B & X = Z \/ W ) by SETFAM_1:def 4, A3;
W \/ Y in UNION B,C by A3, A4, SETFAM_1:def 4;
then Z \/ (W \/ Y) in UNION A,(UNION B,C) by A4, SETFAM_1:def 4;
hence x in A _\/_ (B _\/_ C) by A3, A4, XBOOLE_1:4; :: thesis: verum

end;

A _\/_ (B _\/_ C) c= (A _\/_ B) _\/_ C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A _\/_ (B _\/_ C) or x in (A _\/_ B) _\/_ C )
assume x in A _\/_ (B _\/_ C) ; :: thesis: x in (A _\/_ B) _\/_ C
then consider X, Y being set such that
A5: ( X in A & Y in UNION B,C & x = X \/ Y ) by SETFAM_1:def 4;
consider Z, W being set such that
A6: ( Z in B & W in C & Y = Z \/ W ) by SETFAM_1:def 4, A5;
X \/ Z in UNION A,B by A5, A6, SETFAM_1:def 4;
then (X \/ Z) \/ W in UNION (UNION A,B),C by A6, SETFAM_1:def 4;
hence x in (A _\/_ B) _\/_ C by A5, A6, XBOOLE_1:4; :: thesis: verum

end;

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