:: deftheorem Def4 defines EqRel DICKSON:def 4 :
for R being RelStr st R is quasi_ordered holds
EqRel R = the InternalRel of R /\ ( the InternalRel of R ~);