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