let
X
,
x
be
set
;
:: thesis:
(
x
in
X
implies
(
X
\
{
x
}
)
\/
{
x
}
=
X
)
assume
x
in
X
;
:: thesis:
(
X
\
{
x
}
)
\/
{
x
}
=
X
then
A1
:
{
x
}
is
Subset
of
X
by
SUBSET_1:41
;
{
x
}
\/
(
X
\
{
x
}
)
=
{
x
}
\/
X
by
XBOOLE_1:39
.=
X
by
A1
,
XBOOLE_1:12
;
hence
(
X
\
{
x
}
)
\/
{
x
}
=
X
;
:: thesis:
verum