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