let U be non empty set ; 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; (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
A1:
(A _/\_ B) _/\_ C c= A _/\_ (B _/\_ C)
proof
let x be
set ;
TARSKI:def 3 ( not x in (A _/\_ B) _/\_ C or x in A _/\_ (B _/\_ C) )
assume
x in (A _/\_ B) _/\_ C
;
x in A _/\_ (B _/\_ C)
then consider X,
Y being
set such that A3:
(
X in INTERSECTION A,
B &
Y in C &
x = X /\ Y )
by SETFAM_1:def 5;
consider Z,
W being
set such that A4:
(
Z in A &
W in B &
X = Z /\ W )
by SETFAM_1:def 5, A3;
W /\ Y in INTERSECTION B,
C
by A3, A4, SETFAM_1:def 5;
then
Z /\ (W /\ Y) in INTERSECTION A,
(INTERSECTION B,C)
by A4, SETFAM_1:def 5;
hence
x in A _/\_ (B _/\_ C)
by A3, A4, XBOOLE_1:16;
verum
end;
A _/\_ (B _/\_ C) c= (A _/\_ B) _/\_ C
proof
let x be
set ;
TARSKI:def 3 ( not x in A _/\_ (B _/\_ C) or x in (A _/\_ B) _/\_ C )
assume
x in A _/\_ (B _/\_ C)
;
x in (A _/\_ B) _/\_ C
then consider X,
Y being
set such that A5:
(
X in A &
Y in INTERSECTION B,
C &
x = X /\ Y )
by SETFAM_1:def 5;
consider Z,
W being
set such that A6:
(
Z in B &
W in C &
Y = Z /\ W )
by SETFAM_1:def 5, A5;
X /\ Z in INTERSECTION A,
B
by A5, A6, SETFAM_1:def 5;
then
(X /\ Z) /\ W in INTERSECTION (INTERSECTION A,B),
C
by A6, SETFAM_1:def 5;
hence
x in (A _/\_ B) _/\_ C
by A5, A6, XBOOLE_1:16;
verum
end;
hence
(A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)
by A1, XBOOLE_0:def 10; verum