theorem Th3: :: TREES_A:3

for T being Tree
for P being AntiChain_of_Prefixes of T holds { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } c= { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 }