for X being real-membered set
for a being Real holds card X = card (a ++ X) by Th1, CARD_1:5;