{P : Type u_2} →
  {inst : LE P} →
    {P_1 : Sort u} →
      {toLowerSet : LowerSet P} →
        {nonempty' : toLowerSet.carrier.Nonempty} →
          {directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier} →
            {toLowerSet' : LowerSet P} →
              {nonempty'' : toLowerSet'.carrier.Nonempty} →
                {directed'' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet'.carrier} →
                  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' } =
                      { toLowerSet := toLowerSet', nonempty' := nonempty'', directed' := directed'' } →
                    (toLowerSet ≍ toLowerSet' → P_1) → P_1