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

A1: 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;

A4: now

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

end;

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

end;

thus height (elementary_tree (n + 1)) = 1 by A1, Def15; :: thesis: verum