∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β]
  [inst_4 : LE γ] [inst_5 : OrderTop γ] (g : TopHom β γ) (f : TopHom α β),
  TopHom.dual (g.comp f) = (TopHom.dual g).comp (TopHom.dual f)