theorem Th55: :: ORDINAL7:42

for a, b being Ordinal st a in b holds
b -leading_coeff a = a