take 1TopSp the non empty set ; :: thesis: ( not 1TopSp the non empty set is empty & 1TopSp the non empty set is finite-ind )
thus ( not 1TopSp the non empty set is empty & 1TopSp the non empty set is finite-ind ) ; :: thesis: verum