let n be Element of NAT ; :: thesis: for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Element of 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 Element of NAT st
( k < n & p = <*k*> ) )
assume A1: p in elementary_tree n ; :: thesis: ( p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) )
A2: ( p in {{} } or p in { <*k*> where k is Element of NAT : k < n } ) by A1, XBOOLE_0:def 3;
A3: ( p in { <*k*> where k is Element of NAT : k < n } implies ex k being Element of NAT st
( p = <*k*> & k < n ) ) ;
thus ( p = {} or ex k being Element of NAT st
( k < n & p = <*k*> ) ) by A2, A3, TARSKI:def 1; :: thesis: verum