Definition. power_eq
power M = {A | A ⊆ M}