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