let s be Surreal-Sequence; :: thesis: ( s is strictly_decreasing iff Unique_No s is strictly_decreasing )
set U = Unique_No s;
A1: dom s = dom (Unique_No s) by Def9;
thus ( s is strictly_decreasing implies Unique_No s is strictly_decreasing ) :: thesis: ( Unique_No s is strictly_decreasing implies s is strictly_decreasing )

proof

assume A2: s is strictly_decreasing ; :: thesis: Unique_No s is strictly_decreasing
let A, B be Ordinal; :: according to SURREALC:def 11 :: thesis: ( not A in B or not B in dom (Unique_No s) or for b₁, b₂ being set holds
( not b₁ = (Unique_No s) . A or not b₂ = (Unique_No s) . B or not b₁ <= b₂ ) )
assume A3: ( A in B & B in dom (Unique_No s) ) ; :: thesis: for b₁, b₂ being set holds
( not b₁ = (Unique_No s) . A or not b₂ = (Unique_No s) . B or not b₁ <= b₂ )
let sa, sb be Surreal; :: thesis: ( not sa = (Unique_No s) . A or not sb = (Unique_No s) . B or not sa <= sb )
assume A4: ( sa = (Unique_No s) . A & sb = (Unique_No s) . B ) ; :: thesis: not sa <= sb
A5: ( s . A = s .. A & s . B = s .. B ) by A3, A1, ORDINAL1:10, Def5;
( sa = Unique_No (s .. A) & sb = Unique_No (s .. B) ) by A1, A4, A3, ORDINAL1:10, Def9;
then A6: ( sa == s .. A & sb == s .. B ) by SURREALO:def 10;
then sb < s .. A by A5, A1, A2, A3, SURREALC:def 11, SURREALO:9;
hence not sa <= sb by A6, SURREALO:9; :: thesis: verum

end;

assume A7: Unique_No s is strictly_decreasing ; :: thesis: s is strictly_decreasing
let A, B be Ordinal; :: according to SURREALC:def 11 :: thesis: ( not A in B or not B in dom s or for b₁, b₂ being set holds
( not b₁ = s . A or not b₂ = s . B or not b₁ <= b₂ ) )
assume A8: ( A in B & B in dom s ) ; :: thesis: for b₁, b₂ being set holds
( not b₁ = s . A or not b₂ = s . B or not b₁ <= b₂ )
let sa, sb be Surreal; :: thesis: ( not sa = s . A or not sb = s . B or not sa <= sb )
assume A9: ( sa = s . A & sb = s . B ) ; :: thesis: not sa <= sb
A10: ( (Unique_No s) . A = (Unique_No s) .. A & (Unique_No s) . B = (Unique_No s) .. B ) by A8, A1, Def5, ORDINAL1:10;
( (Unique_No s) .. A = Unique_No (s .. A) & (Unique_No s) .. B = Unique_No (s .. B) & sa = s .. A & sb = s .. B ) by A10, A9, A8, ORDINAL1:10, Def9, Def5;
then A11: ( (Unique_No s) .. A == sa & (Unique_No s) .. B == sb ) by SURREALO:def 10;
then sb < (Unique_No s) .. A by A10, A1, A7, A8, SURREALC:def 11, SURREALO:9;
hence not sa <= sb by A11, SURREALO:9; :: thesis: verum