∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) c d →
      (AntisymmRel (fun x1 x2 => x1 ≤ x2) a c ↔ AntisymmRel (fun x1 x2 => x1 ≤ x2) b d)