let
X
,
Y
,
Z
be
set
;
:: thesis:
X
/\
Y
c=
X
\/
Z
(
X
/\
Y
c=
X
&
X
c=
X
\/
Z
)
by
Th7
,
Th17
;
hence
X
/\
Y
c=
X
\/
Z
;
:: thesis:
verum