theorem :: TREES_1:43

for fT being finite Tree st height fT = 0 holds
fT = elementary_tree 0