:: deftheorem defines elementary_tree TREES_1:def 4 :
for n being Nat holds elementary_tree n = { <*k*> where k is Nat : k < n } \/ {{}};