nt ==> <*(root-label tl),(root-label tr)*> by Def1, Lm3;
then nt ==> roots <*tl,tr*> by BINTREE1:2;
then nt -tree <*tl,tr*> in TS SCM-AE by DTCONSTR:def 1;
hence nt -tree (tl,tr) is bin-term by TREES_4:def 6; :: thesis: verum