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