let
X
be
Subset
of
T
;
:: according to
ROUGHS_2:def 17
:: thesis:
(
ClMap
T
)
.
X
is
closed
(
ClMap
T
)
.
X
=
Cl
X
by
Def15
;
hence
(
ClMap
T
)
.
X
is
closed
;
:: thesis:
verum