let A be RelStr ; :: thesis: for B being Subset of A

for s being FinSequence of A

for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let B be Subset of A; :: thesis: for s being FinSequence of A

for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let s be FinSequence of A; :: thesis: for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let x be Element of A; :: thesis: ( B = {x} & s = <*x*> implies ( s is B -asc_ordering & s is B -desc_ordering ) )

assume that

A1: B = {x} and

A2: s = <*x*> ; :: thesis: ( s is B -asc_ordering & s is B -desc_ordering )

A3: rng s = B by A1, A2, FINSEQ_1:38;

A4: s is one-to-one by A2;

for n, m being Nat st n in dom s & m in dom s & n < m holds

( s /. n <= s /. m & s /. m <= s /. n )

hence ( s is B -asc_ordering & s is B -desc_ordering ) by A3, A4; :: thesis: verum

for s being FinSequence of A

for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let B be Subset of A; :: thesis: for s being FinSequence of A

for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let s be FinSequence of A; :: thesis: for x being Element of A st B = {x} & s = <*x*> holds

( s is B -asc_ordering & s is B -desc_ordering )

let x be Element of A; :: thesis: ( B = {x} & s = <*x*> implies ( s is B -asc_ordering & s is B -desc_ordering ) )

assume that

A1: B = {x} and

A2: s = <*x*> ; :: thesis: ( s is B -asc_ordering & s is B -desc_ordering )

A3: rng s = B by A1, A2, FINSEQ_1:38;

A4: s is one-to-one by A2;

for n, m being Nat st n in dom s & m in dom s & n < m holds

( s /. n <= s /. m & s /. m <= s /. n )

proof

then
( s is weakly-ascending & s is weakly-descending )
;
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies ( s /. n <= s /. m & s /. m <= s /. n ) )

assume that

A5: n in dom s and

A6: m in dom s and

A7: n < m ; :: thesis: ( s /. n <= s /. m & s /. m <= s /. n )

dom s = {1} by A2, FINSEQ_1:38, FINSEQ_1:2;

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

hence ( s /. n <= s /. m & s /. m <= s /. n ) by A7; :: thesis: verum

end;assume that

A5: n in dom s and

A6: m in dom s and

A7: n < m ; :: thesis: ( s /. n <= s /. m & s /. m <= s /. n )

dom s = {1} by A2, FINSEQ_1:38, FINSEQ_1:2;

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

hence ( s /. n <= s /. m & s /. m <= s /. n ) by A7; :: thesis: verum

hence ( s is B -asc_ordering & s is B -desc_ordering ) by A3, A4; :: thesis: verum