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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T | (<*> NAT ) or x in T )
assume A2: x in T | (<*> NAT ) ; :: thesis: x in T
reconsider p = x as Element of T | (<*> NAT ) by A2;
A3: {} ^ p = p by FINSEQ_1:47;
thus x in T by A1, A3, Def9; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in T | (<*> NAT ) )
assume A4: x in T ; :: thesis: x in T | (<*> NAT )
reconsider p = x as Element of T by A4;
A5: {} ^ p = p by FINSEQ_1:47;
thus x in T | (<*> NAT ) by A1, A5, Def9; :: thesis: verum