let a, b be Ordinal; :: thesis: ( a in b implies b -leading_coeff a = a )
assume A1: a in b ; :: thesis: b -leading_coeff a = a

per cases ( 0 in a or not 0 in a ) ;

suppose 0 in a ; :: thesis: b -leading_coeff a = a

thus b -leading_coeff a = a div^ (exp (b,0)) by A1, Th21
.= a div^ 1 by ORDINAL2:43
.= a by ORDINAL3:71 ; :: thesis: verum

end;

suppose not 0 in a ; :: thesis: b -leading_coeff a = a

then ( a = 0 or a in 0 ) by ORDINAL1:14;
hence b -leading_coeff a = a by ORDINAL3:70; :: thesis: verum

end;

end;