set T = the finite Tree;
take { the finite Tree} ; :: thesis: ( { the finite Tree} is finite & { the finite Tree} is constituted-Trees & { the finite Tree} is constituted-FinTrees & not { the finite Tree} is empty )
thus ( { the finite Tree} is finite & { the finite Tree} is constituted-Trees & { the finite Tree} is constituted-FinTrees & not { the finite Tree} is empty ) by Th12, Th13; :: thesis: verum