:: deftheorem Def3 defines Tree-like TREES_1:def 3 :
for X being set holds
( X is Tree-like iff ( X c= NAT * & ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) ) );