let T be Tree; :: thesis: ( {} in T & <*> NAT in T )
consider x being Element of T;
reconsider x = x as FinSequence of NAT ;
x in T ;
then A2: {} ^ x in T by FINSEQ_1:47;
{} = <*> NAT ;
hence ( {} in T & <*> NAT in T ) by A2, Th46; :: thesis: verum