theorem Th43: :: POLYALGX:43

for B being Subset of (Bags 1) holds card B = card (BagN1 .: B)