theorem Th7: :: DICKSON:8

for R being RelStr
for x, y being Element of R st R is quasi_ordered holds
( x in Class ((EqRel R),y) iff ( x <= y & y <= x ) )