for T being finite-branching Tree holds
( T is finite iff ex n being Nat st T -level n = {} )