Q:\H\H-ON.TXT          2001 March 24

When the axiom of regularity holds, one has OMEGA = H(FULL).  Without
the axiom of regularity, we can immediately deduce from results obtained
earlier that:

subclass(OMEGA,intersection(REGULAR,H(FULL))).

It is natural to ask if this inclusion can be sharpened to an equation.
This is indeed the case; to prove it, one needs to use Theorem TC-REG-2
which I have added to the TC\2 group.

After proving this sharper result, Theorem H-ON-3, this becomes a
demodulator which causes the weaker result H-ON-2 to be removed.