feat(set_theory/zfc/basic): define `hereditarily` (#18328)
We will define von Neumann ordinals as hereditarily transitive sets in #18329. Also there are [hereditarily finite sets](https://en.wikipedia.org/wiki/Hereditarily_finite_set) and [hereditarily countable sets](https://en.wikipedia.org/wiki/Hereditarily_countable_set) in set theory.
Co-authored-by: Violeta Hernández [vi.hdz.p@gmail.com](mailto:vi.hdz.p@gmail.com)
