∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : LinearOrder β] {f g : α → β} {a b : β},
  Antitone f → Monotone g → IsGLB (Set.range f) a → IsLUB (Set.range g) b → ⋃ x, Set.Ioo (f x) (g x) = Set.Ioo a b