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

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 Th28, 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 Th28, TARSKI:def 1;
hence len p <= 0 ; :: thesis: verum

end;

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