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 A1: x <= y ; :: thesis: y <= x
set cR = the carrier of R;
set iR = the InternalRel of R;
A2: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
A3: [x,y] in the InternalRel of R by A1, ORDERS_2:def 5;
then ( x in the carrier of R & y in the carrier of R ) by ZFMISC_1:87;
then [y,x] in the InternalRel of R by A2, A3;
hence y <= x by ORDERS_2:def 5; :: thesis: verum