theorem Th6: :: TREES_A:6

for T, T1 being Tree
for P being AntiChain_of_Prefixes of T holds P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P }