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