theorem Th47: :: TREES_1:48

for fT being finite Tree
for t being Element of fT st t <> {} holds
height (fT | t) < height fT