let R be Relation; :: thesis: for a, b being object st R reduces a,b holds
R ~ reduces b,a
let a, b be object ; :: thesis: ( R reduces a,b implies R ~ reduces b,a )
given p being RedSequence of R such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def 3 :: thesis: R ~ reduces b,a
reconsider q = Rev p as RedSequence of R ~ by Th9;
take q ; :: according to REWRITE1:def 3 :: thesis: ( q . 1 = b & q . (len q) = a )
1 in dom q by FINSEQ_5:6;
hence q . 1 = p . (((len p) - 1) + 1) by FINSEQ_5:def 3
.= b by A2 ;
:: thesis: q . (len q) = a
( len q in dom q & len q = len p ) by FINSEQ_5:6, FINSEQ_5:def 3;
hence q . (len q) = p . (((len p) - (len p)) + 1) by FINSEQ_5:def 3
.= a by A1 ;
:: thesis: verum