consider T being finite Tree;
take
{T}
; ( {T} is finite & {T} is constituted-Trees & {T} is constituted-FinTrees & not {T} is empty )
thus
( {T} is finite & {T} is constituted-Trees & {T} is constituted-FinTrees & not {T} is empty )
by Th13, Th14; verum