let X be real-membered set ; :: thesis: for a being real number holds card X = card (a ++ X)
let a be real number ; :: thesis: card X = card (a ++ X)
X,a ++ X are_equipotent by Th1;
hence card X = card (a ++ X) by CARD_1:21; :: thesis: verum