theorem :: POLNOT_1:48

for B, C being antichain
for P being FinSequence-membered set st P is B -headed & B c= C holds
P is C -headed by Th47;