let R be symmetric RelStr ; :: thesis: for x, y being set st the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x

set IR = the InternalRel of R;

let x, y be set ; :: thesis: ( the InternalRel of R reduces x,y implies the InternalRel of R reduces y,x )

A1: the InternalRel of R = the InternalRel of R ~ by RELAT_2:13;

assume the InternalRel of R reduces x,y ; :: thesis: the InternalRel of R reduces y,x

then consider p being RedSequence of the InternalRel of R such that

A2: p . 1 = x and

A3: p . (len p) = y by REWRITE1:def 3;

reconsider p = p as FinSequence ;

A4: (Rev p) . (len p) = x by A2, FINSEQ_5:62;

the InternalRel of R reduces y,x

the InternalRel of R reduces y,x

set IR = the InternalRel of R;

let x, y be set ; :: thesis: ( the InternalRel of R reduces x,y implies the InternalRel of R reduces y,x )

A1: the InternalRel of R = the InternalRel of R ~ by RELAT_2:13;

assume the InternalRel of R reduces x,y ; :: thesis: the InternalRel of R reduces y,x

then consider p being RedSequence of the InternalRel of R such that

A2: p . 1 = x and

A3: p . (len p) = y by REWRITE1:def 3;

reconsider p = p as FinSequence ;

A4: (Rev p) . (len p) = x by A2, FINSEQ_5:62;

the InternalRel of R reduces y,x

proof

hence
the InternalRel of R reduces y,x
; :: thesis: verum
reconsider q = Rev p as RedSequence of the InternalRel of R by A1, REWRITE1:9;

( q . 1 = y & q . (len q) = x ) by A3, A4, FINSEQ_5:62, FINSEQ_5:def 3;

hence the InternalRel of R reduces y,x by REWRITE1:def 3; :: thesis: verum

end;( q . 1 = y & q . (len q) = x ) by A3, A4, FINSEQ_5:62, FINSEQ_5:def 3;

hence the InternalRel of R reduces y,x by REWRITE1:def 3; :: thesis: verum