for B, C being antichain
for p being FinSequence st p is B -headed & B c= C holds
p is C -headed ;