let
i
be
object
;
:: according to
PBOOLE:def 13
:: thesis:
( not
i
in
I
or not
(
X
(\/)
Y
)
.
i
is
empty
)
assume
A1
:
i
in
I
;
:: thesis:
not
(
X
(\/)
Y
)
.
i
is
empty
then
(
X
(\/)
Y
)
.
i
=
(
X
.
i
)
\/
(
Y
.
i
)
by
PBOOLE:def 4
;
hence
not
(
X
(\/)
Y
)
.
i
is
empty
by
A1
;
:: thesis:
verum