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