theorem Th52: :: ORDINAL7:39

for a being Ordinal holds 0 -leading_coeff a = a