dsimp [BddAbove, upperBounds]
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ BddAbove c
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}