let S be surreal-membered ==_distinct set ; :: thesis: for A being Subset of (RevSurrStr S) holds
( A is desc_ordering iff A is well-ordering )
let A be Subset of (RevSurrStr S); :: thesis: ( A is desc_ordering iff A is well-ordering )
set RS = RevSurrStr S;
set I = the InternalRel of (RevSurrStr S);
A1: the carrier of (RevSurrStr S) = S by Def10;
A2: field the InternalRel of (RevSurrStr S) = S by Th41;
A3: field ( the InternalRel of (RevSurrStr S) |_2 A) = A by A1, Th40;
thus ( A is desc_ordering implies A is well-ordering ) :: thesis: ( A is well-ordering implies A is desc_ordering )

proof

assume A is desc_ordering ; :: thesis: A is well-ordering
then consider s being strictly_decreasing Surreal-Sequence such that
A4: rng s = A ;
reconsider t = s as Sequence of field the InternalRel of (RevSurrStr S) by A1, A4, Th42;
A5: t is increasing by A1, A4, Th42;
( the InternalRel of (RevSurrStr S) |_2 A is_reflexive_in A & the InternalRel of (RevSurrStr S) |_2 A is_antisymmetric_in A ) by WELLORD1:15, WELLORD1:18, A3, RELAT_2:def 9, RELAT_2:def 12;
hence A is well-ordering by A4, A5, A1, A2, Th24; :: thesis: verum

end;

assume A is well-ordering ; :: thesis: A is desc_ordering
then consider s being Sequence of field the InternalRel of (RevSurrStr S) such that
A6: ( rng s = A & s is increasing ) by A1, A2, Th24;
reconsider t = s as Surreal-Sequence by A6, SURREALC:def 9;
t is strictly_decreasing by A6, A1, Th42;
hence A is desc_ordering by A6; :: thesis: verum