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

for s being FinSequence of A st s is B -desc_ordering & C c= B holds

ex s2 being FinSequence of A st s2 is C -desc_ordering

let B, C be Subset of A; :: thesis: for s being FinSequence of A st s is B -desc_ordering & C c= B holds

ex s2 being FinSequence of A st s2 is C -desc_ordering

let s be FinSequence of A; :: thesis: ( s is B -desc_ordering & C c= B implies ex s2 being FinSequence of A st s2 is C -desc_ordering )

assume that

A1: s is B -desc_ordering and

A2: C c= B ; :: thesis: ex s2 being FinSequence of A st s2 is C -desc_ordering

Rev (Rev s) is B -desc_ordering by A1;

then Rev s is B -asc_ordering by Th75;

then consider s2 being FinSequence of A such that

A3: s2 is C -asc_ordering by A2, Th80;

take Rev s2 ; :: thesis: Rev s2 is C -desc_ordering

thus Rev s2 is C -desc_ordering by A3, Th75; :: thesis: verum

for s being FinSequence of A st s is B -desc_ordering & C c= B holds

ex s2 being FinSequence of A st s2 is C -desc_ordering

let B, C be Subset of A; :: thesis: for s being FinSequence of A st s is B -desc_ordering & C c= B holds

ex s2 being FinSequence of A st s2 is C -desc_ordering

let s be FinSequence of A; :: thesis: ( s is B -desc_ordering & C c= B implies ex s2 being FinSequence of A st s2 is C -desc_ordering )

assume that

A1: s is B -desc_ordering and

A2: C c= B ; :: thesis: ex s2 being FinSequence of A st s2 is C -desc_ordering

Rev (Rev s) is B -desc_ordering by A1;

then Rev s is B -asc_ordering by Th75;

then consider s2 being FinSequence of A such that

A3: s2 is C -asc_ordering by A2, Th80;

take Rev s2 ; :: thesis: Rev s2 is C -desc_ordering

thus Rev s2 is C -desc_ordering by A3, Th75; :: thesis: verum