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