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