let T be Tree; :: thesis: T | (<*> NAT) = T
A1: <*> NAT in T by Th21;
thus T | (<*> NAT) c= T :: according to XBOOLE_0:def 10 :: thesis: T is_a_prefix_of T | (<*> NAT)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T | (<*> NAT) or x in T )
assume x in T | (<*> NAT) ; :: thesis: x in T
then reconsider p = x as Element of T | (<*> NAT) ;
{} ^ p = p by FINSEQ_1:34;
hence x in T by A1, Def6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in T | (<*> NAT) )
assume x in T ; :: thesis: x in T | (<*> NAT)
then reconsider p = x as Element of T ;
{} ^ p = p by FINSEQ_1:34;
hence x in T | (<*> NAT) by A1, Def6; :: thesis: verum