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