{L : Type u_1} →
  [inst : TopologicalSpace L] →
    [inst_1 : Max L] →
      {motive : ContinuousSup L → Sort u} →
        (t : ContinuousSup L) → ((continuous_sup : Continuous fun p => p.1 ⊔ p.2) → motive ⋯) → motive t