let
X
be non
empty
TopSpace
;
:: thesis:
for
A
being
Subset
of
X
holds
MaxADSet
A
c=
Cl
A
let
A
be
Subset
of
X
;
:: thesis:
MaxADSet
A
c=
Cl
A
Cl
A
=
meet
{
F
where
F
is
Subset
of
X
: (
F
is
closed
&
A
c=
F
)
}
by
Th1
;
hence
MaxADSet
A
c=
Cl
A
by
Th58
;
:: thesis:
verum