let k, n be Element of NAT ; :: thesis: ( k < n implies <*k*> in elementary_tree n )
assume A1: k < n ; :: thesis: <*k*> in elementary_tree n
A2: <*k*> in { <*j*> where j is Element of NAT : j < n } by A1;
thus <*k*> in elementary_tree n by A2, XBOOLE_0:def 3; :: thesis: verum