for X being set holds card ([#] (bspace X)) = exp (2,(card X)) by CARD_2:31;