now

thus ex p being FinSequence of NAT st
( p in elementary_tree 0 & len p = 0 ) :: thesis: for p being FinSequence of NAT st p in elementary_tree 0 holds
len p <= 0

proof

take <*> NAT ; :: thesis: ( <*> NAT in elementary_tree 0 & len (<*> NAT ) = 0 )
thus ( <*> NAT in elementary_tree 0 & len (<*> NAT ) = 0 ) by Th56, TARSKI:def 1; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: ( p in elementary_tree 0 implies len p <= 0 )
assume p in elementary_tree 0 ; :: thesis: len p <= 0
then p = {} by Th56, TARSKI:def 1;
hence len p <= 0 ; :: thesis: verum

end;

hence height (elementary_tree 0 ) = 0 by Def15; :: thesis: verum