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