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)

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

A _/\_ (B _/\_ 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 _/\_ C) )

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

then consider X, Y being set such that

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

consider Z, W being set such that

A3: ( Z in A & W in B & X = Z /\ W ) by A2, SETFAM_1:def 5;

W /\ Y in INTERSECTION (B,C) by A2, A3, SETFAM_1:def 5;

then Z /\ (W /\ Y) in INTERSECTION (A,(INTERSECTION (B,C))) by A3, SETFAM_1:def 5;

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

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

then consider X, Y being set such that

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

consider Z, W being set such that

A3: ( Z in A & W in B & X = Z /\ W ) by A2, SETFAM_1:def 5;

W /\ Y in INTERSECTION (B,C) by A2, A3, SETFAM_1:def 5;

then Z /\ (W /\ Y) in INTERSECTION (A,(INTERSECTION (B,C))) by A3, SETFAM_1:def 5;

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

proof

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

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

consider Z, W being set such that

A5: ( Z in B & W in C & Y = Z /\ W ) by A4, SETFAM_1:def 5;

X /\ Z in INTERSECTION (A,B) by A4, A5, SETFAM_1:def 5;

then (X /\ Z) /\ W in INTERSECTION ((INTERSECTION (A,B)),C) by A5, SETFAM_1:def 5;

hence x in (A _/\_ B) _/\_ C by A4, A5, XBOOLE_1:16; :: thesis: verum

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

then consider X, Y being set such that

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

consider Z, W being set such that

A5: ( Z in B & W in C & Y = Z /\ W ) by A4, SETFAM_1:def 5;

X /\ Z in INTERSECTION (A,B) by A4, A5, SETFAM_1:def 5;

then (X /\ Z) /\ W in INTERSECTION ((INTERSECTION (A,B)),C) by A5, SETFAM_1:def 5;

hence x in (A _/\_ B) _/\_ C by A4, A5, XBOOLE_1:16; :: thesis: verum