How can I define the cardinality of a set as the number of elements in a set Susing the notation |S| using TLA.