let R be symmetric RelStr ; :: thesis: for x, y being Element of R st x <= y holds
y <= x
let x, y be Element of R; :: thesis: ( x <= y implies y <= x )
assume A: x <= y ; :: thesis: y <= x
set cR = the carrier of R;
set iR = the InternalRel of R;
B: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 4;
C: [x,y] in the InternalRel of R by A, ORDERS_2:def 9;
then ( x in the carrier of R & y in the carrier of R ) by ZFMISC_1:106;
then [y,x] in the InternalRel of R by B, C, RELAT_2:def 3;
hence y <= x by ORDERS_2:def 9; :: thesis: verum