let R be symmetric RelStr ; :: thesis: for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R
let x, y be set ; :: thesis: ( x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R implies [y,x] in the InternalRel of R )
set cR = the carrier of R;
set iR = the InternalRel of R;
assume that
A1: x in the carrier of R and
A2: y in the carrier of R and
A3: [x,y] in the InternalRel of R ; :: thesis: [y,x] in the InternalRel of R
the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
hence [y,x] in the InternalRel of R by A1, A2, A3, RELAT_2:def 3; :: thesis: verum