let n be Nat; :: thesis: for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Nat st
( k < n & p = <*k*> ) )
let p be FinSequence of NAT ; :: thesis: ( not p in elementary_tree n or p = {} or ex k being Nat st
( k < n & p = <*k*> ) )
assume p in elementary_tree n ; :: thesis: ( p = {} or ex k being Nat st
( k < n & p = <*k*> ) )
then A1: ( p in {{}} or p in { <*k*> where k is Nat : k < n } ) by XBOOLE_0:def 3;
( p in { <*k*> where k is Nat : k < n } implies ex k being Nat st
( p = <*k*> & k < n ) ) ;
hence ( p = {} or ex k being Nat st
( k < n & p = <*k*> ) ) by A1, TARSKI:def 1; :: thesis: verum