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

for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds

s1 = s2

let B be Subset of A; :: thesis: for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds

s1 = s2

let s1, s2 be FinSequence of A; :: thesis: ( s1 is B -desc_ordering & s2 is B -desc_ordering implies s1 = s2 )

assume ( s1 is B -desc_ordering & s2 is B -desc_ordering ) ; :: thesis: s1 = s2

then ( Rev (Rev s1) is B -desc_ordering & Rev (Rev s2) is B -desc_ordering ) ;

then ( Rev s1 is B -asc_ordering & Rev s2 is B -asc_ordering ) by Th75;

then A1: Rev s1 = Rev s2 by Th77;

thus s1 = Rev (Rev s2) by A1

.= s2 ; :: thesis: verum

for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds

s1 = s2

let B be Subset of A; :: thesis: for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds

s1 = s2

let s1, s2 be FinSequence of A; :: thesis: ( s1 is B -desc_ordering & s2 is B -desc_ordering implies s1 = s2 )

assume ( s1 is B -desc_ordering & s2 is B -desc_ordering ) ; :: thesis: s1 = s2

then ( Rev (Rev s1) is B -desc_ordering & Rev (Rev s2) is B -desc_ordering ) ;

then ( Rev s1 is B -asc_ordering & Rev s2 is B -asc_ordering ) by Th75;

then A1: Rev s1 = Rev s2 by Th77;

thus s1 = Rev (Rev s2) by A1

.= s2 ; :: thesis: verum