To be sure about the answer you should refer to the definition of ATOMS and the language of PROP. Most likely, ATOMS is a countably infinite set such as . One rarely considers finite or uncountable sets of atoms (an exception that comes to mind is the Löwenheim–Skolem theorem).

If ATOMS is infinite, then Card(PROP) = Card(ATOMS). Of course, if ATOMS is finite, then PROP is countably infinite.

In fact, even if ATOMS is not equinumerous with PROP, as is the case when ATOMS is finite, the sets of valuations on ATOMS and on PROP are equinumerous. This is because the mapping that extends a valuation from ATOMS to PROP is a bijection.