theorem Th40: :: POLYALGX:40

for B being Subset of NAT holds card B = card (NBag1 .: B)