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
proof
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;
hence <*x*> is ascending ; :: thesis: ( <*x*> is weakly-ascending & <*x*> is descending & <*x*> is weakly-descending )
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
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;
hence <*x*> is descending ; :: thesis: <*x*> is weakly-descending
hence <*x*> is weakly-descending ; :: thesis: verum