let k, n be Element of 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 Element of NAT : j < n } ;
hence <*k*> in elementary_tree n by XBOOLE_0:def 3; :: thesis: verum