theorem Th47: :: TREES_9:47

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