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

for s1 being FinSequence of A

for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let B, C be Subset of A; :: thesis: for s1 being FinSequence of A

for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let s1 be FinSequence of A; :: thesis: for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let x be Element of A; :: thesis: ( s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) implies ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering ) )

assume that

A1: s1 is C -desc_ordering and

A2: ( not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) ) ; :: thesis: ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

Rev (Rev s1) is C -desc_ordering by A1;

then Rev s1 is C -asc_ordering by Th75;

then consider s2 being FinSequence of A such that

A3: s2 = <*x*> ^ (Rev s1) and

A4: s2 is B -asc_ordering by A2, Th85;

take Rev s2 ; :: thesis: ( Rev s2 = s1 ^ <*x*> & Rev s2 is B -desc_ordering )

thus Rev s2 = (Rev (Rev s1)) ^ (Rev <*x*>) by A3, FINSEQ_5:64

.= s1 ^ <*x*> by FINSEQ_5:60 ; :: thesis: Rev s2 is B -desc_ordering

thus Rev s2 is B -desc_ordering by A4, Th75; :: thesis: verum

for s1 being FinSequence of A

for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let B, C be Subset of A; :: thesis: for s1 being FinSequence of A

for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let s1 be FinSequence of A; :: thesis: for x being Element of A st s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

let x be Element of A; :: thesis: ( s1 is C -desc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) implies ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering ) )

assume that

A1: s1 is C -desc_ordering and

A2: ( not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

x <= y ) ) ; :: thesis: ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -desc_ordering )

Rev (Rev s1) is C -desc_ordering by A1;

then Rev s1 is C -asc_ordering by Th75;

then consider s2 being FinSequence of A such that

A3: s2 = <*x*> ^ (Rev s1) and

A4: s2 is B -asc_ordering by A2, Th85;

take Rev s2 ; :: thesis: ( Rev s2 = s1 ^ <*x*> & Rev s2 is B -desc_ordering )

thus Rev s2 = (Rev (Rev s1)) ^ (Rev <*x*>) by A3, FINSEQ_5:64

.= s1 ^ <*x*> by FINSEQ_5:60 ; :: thesis: Rev s2 is B -desc_ordering

thus Rev s2 is B -desc_ordering by A4, Th75; :: thesis: verum