let
X
be non
empty
TopSpace
;
:: thesis:
for
x
being
Point
of
X
holds
x
in
Cl
{
x
}
let
x
be
Point
of
X
;
:: thesis:
x
in
Cl
{
x
}
(
x
in
{
x
}
&
{
x
}
c=
Cl
{
x
}
)
by
PRE_TOPC:18
,
TARSKI:def 1
;
hence
x
in
Cl
{
x
}
;
:: thesis:
verum