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 [x,y] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
then A2: ( [x,y] in the InternalRel of R & [x,y] in the InternalRel of R ~ ) by XBOOLE_0:def 4;
hence x <= y by ORDERS_2:def 9; :: thesis: y <= x
[y,x] in the InternalRel of R by A2, RELAT_1:def 7;
hence y <= x by ORDERS_2:def 9; :: thesis: verum

end;

assume ( x <= y & y <= x ) ; :: thesis: x in Class (EqRel R),y
then ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by ORDERS_2:def 9;
then ( [x,y] in the InternalRel of R & [x,y] in the InternalRel of R ~ ) by RELAT_1:def 7;
then [x,y] in the InternalRel of R /\ (the InternalRel of R ~ ) by 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