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 Th11a;