set T = the non empty finite TopSpace;
take the non empty finite TopSpace ; :: thesis: ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty )
thus ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty ) ; :: thesis: verum