{L : Type u_1} →
  [inst : TopologicalSpace L] →
    [inst_1 : Lattice L] →
      {motive : TopologicalLattice L → Sort u} →
        ([toContinuousInf : ContinuousInf L] → [toContinuousSup : ContinuousSup L] → motive ⋯) →
          (t : TopologicalLattice L) → motive t