let
X
,
Y
,
Z
,
x
be
set
;
:: thesis:
(
x
in
(
X
\/
Y
)
\/
Z
iff (
x
in
X
or
x
in
Y
or
x
in
Z
) )
set
W
=
(
X
\/
Y
)
\/
Z
;
(
x
in
(
X
\/
Y
)
\/
Z
iff (
x
in
X
\/
Y
or
x
in
Z
) )
by
XBOOLE_0:def 3
;
hence
(
x
in
(
X
\/
Y
)
\/
Z
iff (
x
in
X
or
x
in
Y
or
x
in
Z
) )
by
XBOOLE_0:def 3
;
:: thesis:
verum