nt3 -tree (t1,t2) in TS SCM-AE ;
hence [0,3] -tree (t1,t2) is bin-term ; :: thesis: verum