apply lowerBounds_mono_set h
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s
case a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds t