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