let U be non empty set ; 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; A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
A1:
A _/\_ (B _\/_ C) c= (A _/\_ B) _\/_ (A _/\_ C)
proof
let x be
object ;
TARSKI:def 3 ( not x in A _/\_ (B _\/_ C) or x in (A _/\_ B) _\/_ (A _/\_ C) )
assume
x in A _/\_ (B _\/_ C)
;
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;
verum
end;
(A _/\_ B) _\/_ (A _/\_ C) c= A _/\_ (B _\/_ C)
hence
A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
by A1; verum