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
proof
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;
hence the InternalRel of R reduces y,x ; :: thesis: verum