A1: 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 A2: p in elementary_tree 0 ; :: thesis: len p <= 0
A3: p = {} by A2, Th56, TARSKI:def 1;
thus len p <= 0 by A3; :: thesis: verum

end;

thus height (elementary_tree 0 ) = 0 by A1, Def15; :: thesis: verum