∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictMono f → (∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))) → Order.IsNormal f