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 4;
hence nt -tree tl,tr is bin-term by TREES_4:def 6; :: thesis: verum