theorem Th47: :: POLNOT_1:47

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