:: deftheorem defines -headed POLNOT_1:def 20 :
for B being antichain
for p being FinSequence holds
( p is B -headed iff ex q, r being FinSequence st
( q in B & p = q ^ r ) );