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