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