let s be Surreal-Sequence; :: thesis: for X being surreal-membered ==_distinct set st rng s c= X holds
( s is Sequence of field the InternalRel of (RevSurrStr X) & ( for t being Sequence of field the InternalRel of (RevSurrStr X) st t = s holds
( s is strictly_decreasing iff t is increasing ) ) )
let X be surreal-membered ==_distinct set ; :: thesis: ( rng s c= X implies ( s is Sequence of field the InternalRel of (RevSurrStr X) & ( for t being Sequence of field the InternalRel of (RevSurrStr X) st t = s holds
( s is strictly_decreasing iff t is increasing ) ) ) )
assume A1: rng s c= X ; :: thesis: ( s is Sequence of field the InternalRel of (RevSurrStr X) & ( for t being Sequence of field the InternalRel of (RevSurrStr X) st t = s holds
( s is strictly_decreasing iff t is increasing ) ) )
set R = RevSurrStr X;
set I = the InternalRel of (RevSurrStr X);
field the InternalRel of (RevSurrStr X) = X by Th41;
hence s is Sequence of field the InternalRel of (RevSurrStr X) by A1, RELAT_1:def 19; :: thesis: for t being Sequence of field the InternalRel of (RevSurrStr X) st t = s holds
( s is strictly_decreasing iff t is increasing )
let t be Sequence of field the InternalRel of (RevSurrStr X); :: thesis: ( t = s implies ( s is strictly_decreasing iff t is increasing ) )
assume A2: t = s ; :: thesis: ( s is strictly_decreasing iff t is increasing )
thus ( s is strictly_decreasing implies t is increasing ) :: thesis: ( t is increasing implies s is strictly_decreasing )

proof

assume A3: s is strictly_decreasing ; :: thesis: t is increasing
let A, B be Ordinal; :: according to SURREAL1:def 3 :: thesis: ( A in B & B in dom t implies ( t . A <> t . B & [(t . A),(t . B)] in the InternalRel of (RevSurrStr X) ) )
assume A4: ( A in B & B in dom t ) ; :: thesis: ( t . A <> t . B & [(t . A),(t . B)] in the InternalRel of (RevSurrStr X) )
A in dom t by A4, ORDINAL1:10;
then A5: ( s . A in rng s & s . B in rng s ) by A2, A4, FUNCT_1:def 3;
A6: ( s .. A = s . A & s .. B = s . B ) by A2, A4, ORDINAL1:10, Def5;
hence t . A <> t . B by A2, A3, A4, SURREALC:def 11, SURREALO:3; :: thesis: [(t . A),(t . B)] in the InternalRel of (RevSurrStr X)
s .. B <= s .. A by A6, A2, A3, A4, SURREALC:def 11;
hence [(t . A),(t . B)] in the InternalRel of (RevSurrStr X) by A2, A5, A1, A6, Def10; :: thesis: verum

end;

assume A7: t is increasing ; :: 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 & not sb < sa ) ; :: thesis: contradiction
A in dom s by A8, ORDINAL1:10;
then A10: ( s . A in rng s & s . B in rng s ) by A8, FUNCT_1:def 3;
( sa <> sb & [sa,sb] in the InternalRel of (RevSurrStr X) ) by A7, A2, A8, A9;
then sb == sa by A1, A10, A9, Def10;
hence contradiction by A1, A7, A2, A8, A9, A10, Def11; :: thesis: verum