:: deftheorem defines ^ TREES_3:def 16 :
for T being Tree holds ^ T = tree <*T*>;