Set_is_Equivalent_to_Proper_Subset_of_Power_Set

import Mathlib.Data.Set.Basic
import Mathlib.Logic.Equiv.Defs

theorem Set_is_Equivalent_to_Proper_Subset_of_Power_Set {α : Type _} : ∃ T : Set (Set α), T ⊂ Set.univ ∧ Nonempty (α ≃ T) := by sorry