theorem Th11: :: GROEB_3:11

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)