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