revert h𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card