let n be Nat; :: thesis: height (elementary_tree (n + 1)) = 1
set T = elementary_tree (n + 1);

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

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 Th27; :: thesis: len p = 1
thus len p = 1 by FINSEQ_1:40; :: thesis: verum

end;

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

now :: thesis: ( p in { <*k*> where k is Nat : k < n + 1 } implies len p = 1 )

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

end;

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

end;

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