theorem Th43: :: POLNOT_1:43

for B being antichain
for p, q, r, s being FinSequence st p ^ q = r ^ s & p in B & r in B holds
( p = r & q = s )