theorem Th23: :: PRE_POLY:24

for p being set holds Card <*p*> = <*(card p)*>