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:19;
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; :: thesis: y <= x
[y,x] in the InternalRel of R by A4, RELAT_1:def 7;
hence y <= x ; :: 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;
A8: [x,y] in the InternalRel of R by A5;
[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:19; :: thesis: verum