:: deftheorem Def11 defines AntiChain_of_Prefixes TREES_1:def 11 :
for T being Tree
for b₂ being AntiChain_of_Prefixes holds
( b₂ is AntiChain_of_Prefixes of T iff b₂ c= T );