take
the
topology
of
T
;
:: thesis:
( the
topology
of
T
is
open
& not the
topology
of
T
is
empty
)
thus
( the
topology
of
T
is
open
& not the
topology
of
T
is
empty
) ;
:: thesis:
verum