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 )
proof
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;
then ( s is weakly-ascending & s is weakly-descending ) ;
hence ( s is B -asc_ordering & s is B -desc_ordering ) by A3, A4; :: thesis: verum