take the non empty finite Subset of T ; :: thesis: ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty )
thus ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty ) ; :: thesis: verum