no goals
α : Type u_1
β : Type u_2
γ : Type ?u.187458
ι : Sort ?u.187461
κ : ι → Sort ?u.187466
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : LowerSet α
t t₁ t₂ : LowerSet β
x : α × β
⊢ ↑s₁ ⊆ ↑s₂ ∧ ↑t₁ ⊆ ↑t₂ ∨ ↑s₁ = ∅ ∨ ↑t₁ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥
simp