let
X
be non
empty
TopSpace
;
:: thesis:
for
x
being
Point
of
X
holds
MaxADSet
x
c=
Cl
{
x
}
let
x
be
Point
of
X
;
:: thesis:
MaxADSet
x
c=
Cl
{
x
}
Cl
{
x
}
=
meet
{
F
where
F
is
Subset
of
X
: (
F
is
closed
&
x
in
F
)
}
by
Th2
;
hence
MaxADSet
x
c=
Cl
{
x
}
by
Th47
;
:: thesis:
verum