:: deftheorem defines * SCM_COMP:def 5 :
for t1, t2 being bin-term holds t1 * t2 = [0,2] -tree (t1,t2);