8.1.10 Union interpretation of derived types.
It says that the rule is recursive, which is true, but 
unfortunately it seems that there is no way to start the 
recursion, since in order to deduce one "extended with union
interpretation" judgment, you need to already know some of
the same kind of judgment to supply the hypotheses above the 
line.  

To start a recursion, I tried letting n = m = 0
(this is a trick that is sometimes used to provide seeds
for recursion).  However, in that case, all
hypotheses disappear, and we are left (seemingly) with the 
inference that it is always true that any Type1 is any Type0 
extended with union interpretation of any TypeName0.
So you must not intend that it is permitted for n = m = 0.
(Once again I say, please supply quantifiers on all your 
free variables in your inferences!)

If n > 0 and m = 0, then Type1 is a union of restriction
types (see last judgment above the line), 
and the name of the judgment, "extended with union
interpretation" does not make sense -- I expect to find 
some type extensions, not just restrictions, in the hypotheses.
I conclude that m = 0 is not permitted, so we must have m > 0.

Looking at the example, the example shows that you intend
to make deductions about types with only extension and no
restriction.  I conclude that n = 0 is permitted.

Now lets see if we can actually deduce the example.  
I will reason backwards.  We want to conclude:

  statEnv |- (element a | (element a, element b) is (element a)
             extended with union interpretation of T1

so:

  Type1 = (element a | (element a, element b))
  Type0 = (element a)
  TypeName0 = T1

from the last inference above the line: 

  TypeR,1' = (element a)
  TypeE,1' = (element b)

then

  TypeNameE,1 = T2 because of "define type T2 extends T1 {element b}"

so

  TypeE,1 is the extender part of this definition = (element b)

Now I need to know that 

  statEnv |- (element b) is (element b) extended with union 
             interpretation of T2

but I don't see any way to deduce this.  Probably what you need
is a "seed rule" saying that any type is itself extended with
union interpretation of any typename.  I don't see a way to 
deduce such seeds.

By the way, it would really help if you worked your own example
out to this level of detail and put it in the spec.