consider X being non empty finite Subset of T;
reconsider X = X as Subset of T ;
take X ; :: thesis: ( X is finite & not X is empty )
thus ( X is finite & not X is empty ) ; :: thesis: verum