take { the Element of the non empty set * } ; :: thesis: ( { the Element of the non empty set * } is trivial & { the Element of the non empty set * } is FinSequence-membered & not { the Element of the non empty set * } is empty )
thus ( { the Element of the non empty set * } is trivial & { the Element of the non empty set * } is FinSequence-membered & not { the Element of the non empty set * } is empty ) ; :: thesis: verum