feat(model_theory/skolem): Downward Löwenheim–Skolem (#13723)
Proves the Downward Löwenheim–Skolem theorem: If `s` is a set in an `L`-structure `M` and `κ` an infinite cardinal such that `max (# s, L.card) ≤ κ` and `κ ≤ # M`, then `M` has an elementary substructure containing `s` of cardinality `κ`.
