theorem Th1: :: INT_4:1

for X being real-membered set
for a being Real holds X,a ++ X are_equipotent