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