290 Formalization

7 Cardinality