intro ht x hx u hu
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S → t ≤ ⋂₀ S
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ lowerBounds S
x : Y
hx : x ∈ t
u : Set Y
hu : u ∈ S
⊢ x ∈ u