consider T being non empty finite TopSpace;
take T ; :: thesis: ( T is second-countable & not T is empty )
thus ( T is second-countable & not T is empty ) ; :: thesis: verum