let k, n be Nat; :: thesis: ( k < n implies <*k*> in elementary_tree n )
assume k < n ; :: thesis: <*k*> in elementary_tree n
then <*k*> in { <*j*> where j is Nat : j < n } ;
hence <*k*> in elementary_tree n by XBOOLE_0:def 3; :: thesis: verum