let
X
,
Y
be
set
;
:: thesis:
(
X
is
empty
&
X
<>
Y
implies not
Y
is
empty
)
assume
that
A1
:
X
is
empty
and
A2
:
X
<>
Y
;
:: thesis:
not
Y
is
empty
X
=
{}
by
A1
,
Lm1
;
hence
not
Y
is
empty
by
A2
,
Lm1
;
:: thesis:
verum