let R be RelStr ; :: thesis: for x, y being Element of R st R is quasi_ordered holds
( x in Class (EqRel R),y iff ( x <= y & y <= x ) )
let x, y be Element of R; :: thesis: ( R is quasi_ordered implies ( x in Class (EqRel R),y iff ( x <= y & y <= x ) ) )
assume A1: R is quasi_ordered ; :: thesis: ( x in Class (EqRel R),y iff ( x <= y & y <= x ) )
set IR = the InternalRel of R;

hereby :: thesis: ( x <= y & y <= x implies x in Class (EqRel R),y )

assume x in Class (EqRel R),y ; :: thesis: ( x <= y & y <= x )
then [x,y] in EqRel R by EQREL_1:27;
then A2: [x,y] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
then A3: [x,y] in the InternalRel of R by XBOOLE_0:def 4;
A4: [x,y] in the InternalRel of R ~ by A2, XBOOLE_0:def 4;
thus x <= y by A3, ORDERS_2:def 9; :: thesis: y <= x
[y,x] in the InternalRel of R by A4, RELAT_1:def 7;
hence y <= x by ORDERS_2:def 9; :: thesis: verum

end;

assume that
A5: x <= y and
A6: y <= x ; :: thesis: x in Class (EqRel R),y
A7: [y,x] in the InternalRel of R by A6, ORDERS_2:def 9;
A8: [x,y] in the InternalRel of R by A5, ORDERS_2:def 9;
[x,y] in the InternalRel of R ~ by A7, RELAT_1:def 7;
then [x,y] in the InternalRel of R /\ (the InternalRel of R ~ ) by A8, XBOOLE_0:def 4;
then [x,y] in EqRel R by A1, Def4;
hence x in Class (EqRel R),y by EQREL_1:27; :: thesis: verum