set
X
= the
infinite
set
;
take
CofinTop
the
infinite
set
;
:: thesis:
(
CofinTop
the
infinite
set
is
T_1
& not
CofinTop
the
infinite
set
is
sober
)
thus
(
CofinTop
the
infinite
set
is
T_1
& not
CofinTop
the
infinite
set
is
sober
) ;
:: thesis:
verum