intro
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑{∅}).OrdConnected → ({∅} \₊ {∅}).card ≤ {∅}.card
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜✝ : (↑{∅}).OrdConnected
⊢ ({∅} \₊ {∅}).card ≤ {∅}.card