Q:\DEDEKIND\ALL.TXT

2000 June 12

We are currently using this lex order:

lex([0,id(x),Id,omega,FINITE,DEDEKIND,Q,pair(x,x),singleton(x),
     cart(x,x),intersection(x,x),complement(x),fix(x),D(x),R(x),
     image(x,x),composite(x,x),K,PS,inverse(x),
     ONEONE(x),equal(x,x),member(x,x),subclass(x,x)]).

Theorem DK-OM-Q2 becomes a demodulator which causes Lemma DK-OM-Q1
to be transformed and then removed by subsumption with Theorem IDX-2.