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