let R be symmetric RelStr ; :: thesis: for x, y being set st x in the carrier of R & y in the carrier of R & the InternalRel of R reduces x,y holds
the InternalRel of R reduces y,x
set cR = the carrier of R;
set IR = the InternalRel of R;
let x, y be set ; :: thesis: ( x in the carrier of R & y in the carrier of R & the InternalRel of R reduces x,y implies the InternalRel of R reduces y,x )
assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( not the InternalRel of R reduces x,y or the InternalRel of R reduces y,x )
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
A1: ( p . 1 = x & p . (len p) = y ) by REWRITE1:def 3;
reconsider p = p as FinSequence ;
A2: the InternalRel of R = the InternalRel of R ~ by RELAT_2:30;
A3: ( (Rev p) . (len p) = x & (Rev p) . 1 = y ) by A1, FINSEQ_5:65;
the InternalRel of R reduces y,x

proof

reconsider q = Rev p as RedSequence of the InternalRel of R by A2, REWRITE1:10;
( q . 1 = y & q . (len q) = x ) by A3, 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