∀ {X Y : Preord} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun X => AlexDisc.of (Topology.WithUpperSet ↑X),
                map := fun {X Y} f =>
                  CategoryTheory.ConcreteCategory.ofHom (Topology.WithUpperSet.map (Preord.Hom.hom f)),
                map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 }.comp
            ((CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord)).map
        f)
      ((fun X => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) X).hom
      ((CategoryTheory.Functor.id Preord).map f)