let
T
be non
empty
discrete
TopSpace
;
:: thesis:
(
T
is
separable
iff
T
is
countable
)
(
T
is
separable
iff
card
(
[#]
T
)
c=
omega
)
by
Th10
;
hence
(
T
is
separable
iff
T
is
countable
)
by
TOPGEN_1:2
;
:: thesis:
verum