consider p being non empty Tree-yielding FinTree-yielding FinSequence;
take p ; :: thesis: ( p is Tree-yielding & p is FinTree-yielding & not p is empty )
thus ( p is Tree-yielding & p is FinTree-yielding & not p is empty ) ; :: thesis: verum