theorem :: DICKSON:18

for R, S being non empty RelStr
for m being Function of R,S st R is quasi_ordered & S is antisymmetric & S \~ is well_founded & ( for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ) holds
R \~ is well_founded