:: deftheorem Def1 defines tree TREES_A:def 1 :
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
for b₄ being Tree holds
( b₄ = tree (T,P,T1) iff for q being FinSequence of NAT holds
( q in b₄ iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) );