consider vt being finite DecoratedTree such that
A1: vt is_an_evaluation_of t,f by Th36;
reconsider tf = vt . {} as Element of the Sorts of A . (the_sort_of t) by A1, Th38;
take tf ; :: thesis: ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & tf = vt . {} )
take vt ; :: thesis: ( vt is_an_evaluation_of t,f & tf = vt . {} )
thus ( vt is_an_evaluation_of t,f & tf = vt . {} ) by A1; :: thesis: verum