theorem :: POLNOT_1:49

for B, C being antichain
for p being FinSequence st p is B ^ C -headed holds
p is B -headed