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