let A be non empty RelStr ; :: thesis: for x being Element of A holds

( <*x*> is ascending & <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )

let x be Element of A; :: thesis: ( <*x*> is ascending & <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )

set s = <*x*>;

for n, m being Nat st n in dom <*x*> & m in dom <*x*> & n < m holds

<*x*> /. n <~ <*x*> /. m

hence <*x*> is weakly-ascending ; :: thesis: ( <*x*> is descending & <*x*> is weakly-descending )

for n, m being Nat st n in dom <*x*> & m in dom <*x*> & n < m holds

<*x*> /. m <~ <*x*> /. n

hence <*x*> is weakly-descending ; :: thesis: verum

( <*x*> is ascending & <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )

let x be Element of A; :: thesis: ( <*x*> is ascending & <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )

set s = <*x*>;

for n, m being Nat st n in dom <*x*> & m in dom <*x*> & n < m holds

<*x*> /. n <~ <*x*> /. m

proof

hence
<*x*> is ascending
; :: thesis: ( <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )
let n, m be Nat; :: thesis: ( n in dom <*x*> & m in dom <*x*> & n < m implies <*x*> /. n <~ <*x*> /. m )

assume that

A2: ( n in dom <*x*> & m in dom <*x*> ) and

A3: n < m ; :: thesis: <*x*> /. n <~ <*x*> /. m

( n in {1} & m in {1} ) by A2, FINSEQ_1:38, FINSEQ_1:2;

then ( n = 1 & m = 1 ) by TARSKI:def 1;

hence <*x*> /. n <~ <*x*> /. m by A3; :: thesis: verum

end;assume that

A2: ( n in dom <*x*> & m in dom <*x*> ) and

A3: n < m ; :: thesis: <*x*> /. n <~ <*x*> /. m

( n in {1} & m in {1} ) by A2, FINSEQ_1:38, FINSEQ_1:2;

then ( n = 1 & m = 1 ) by TARSKI:def 1;

hence <*x*> /. n <~ <*x*> /. m by A3; :: thesis: verum

hence <*x*> is weakly-ascending ; :: thesis: ( <*x*> is descending & <*x*> is weakly-descending )

for n, m being Nat st n in dom <*x*> & m in dom <*x*> & n < m holds

<*x*> /. m <~ <*x*> /. n

proof

hence
<*x*> is descending
; :: thesis: <*x*> is weakly-descending
let n, m be Nat; :: thesis: ( n in dom <*x*> & m in dom <*x*> & n < m implies <*x*> /. m <~ <*x*> /. n )

assume that

A4: ( n in dom <*x*> & m in dom <*x*> ) and

A5: n < m ; :: thesis: <*x*> /. m <~ <*x*> /. n

( n in {1} & m in {1} ) by A4, FINSEQ_1:38, FINSEQ_1:2;

then ( n = 1 & m = 1 ) by TARSKI:def 1;

hence <*x*> /. m <~ <*x*> /. n by A5; :: thesis: verum

end;assume that

A4: ( n in dom <*x*> & m in dom <*x*> ) and

A5: n < m ; :: thesis: <*x*> /. m <~ <*x*> /. n

( n in {1} & m in {1} ) by A4, FINSEQ_1:38, FINSEQ_1:2;

then ( n = 1 & m = 1 ) by TARSKI:def 1;

hence <*x*> /. m <~ <*x*> /. n by A5; :: thesis: verum

hence <*x*> is weakly-descending ; :: thesis: verum