Q:\DEDEKIND\DK-OM-Q2.TXT      2000 June 12

I was unable to prove DK-OM-Q2 directly without Lemma DK-OM-Q1.

We got two proofs of DK-OM-Q2 both of which do use the Lemma. The
difference between these two proofs is that for one proof we left the
Lemma on the usable list, while for the other we placed the Lemma in the
set of support. Placing Lemma DK-OM-Q1 in the set of support shortens
the proof dramatically and allows one to assign a much lower value to
max_weight. See the ALTPROOF directory.