set p = the non empty DTree-yielding FinSequence;
take the non empty DTree-yielding FinSequence ; :: thesis: ( the non empty DTree-yielding FinSequence is DTree-yielding & not the non empty DTree-yielding FinSequence is empty )
thus ( the non empty DTree-yielding FinSequence is DTree-yielding & not the non empty DTree-yielding FinSequence is empty ) ; :: thesis: verum