let n be Element of NAT ; :: thesis: height (elementary_tree (n + 1)) = 1
set T = elementary_tree (n + 1);

now

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

proof

take p = <*0 *>; :: thesis: ( p in elementary_tree (n + 1) & len p = 1 )
thus p in elementary_tree (n + 1) by Th55; :: thesis: len p = 1
thus len p = 1 by FINSEQ_1:57; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: ( p in elementary_tree (n + 1) implies len p <= 1 )
assume A2: p in elementary_tree (n + 1) ; :: thesis: len p <= 1
A3: ( p in {{} } implies p = {} ) by TARSKI:def 1;

now

assume p in { <*k*> where k is Element of NAT : k < n + 1 } ; :: thesis: len p = 1
then ex k being Element of NAT st
( p = <*k*> & k < n + 1 ) ;
hence len p = 1 by FINSEQ_1:57; :: thesis: verum

end;

hence len p <= 1 by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

hence height (elementary_tree (n + 1)) = 1 by Def15; :: thesis: verum