let S be surreal-membered desc_ordering set ; :: thesis: Unique_No S is desc_ordering
consider y being strictly_decreasing Surreal-Sequence such that
A1: rng y = S by Def12;
rng (Unique_No y) is desc_ordering ;
hence Unique_No S is desc_ordering by A1, Th37; :: thesis: verum