:: deftheorem Def8 defines -headed POLNOT_1:def 21 :
for B being antichain
for P being FinSequence-membered set holds
( P is B -headed iff for p being FinSequence st p in P holds
p is B -headed );