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;