let b be Ordinal; :: thesis: b -leading_coeff 1 = 1

per cases ( 1 in b or 1 = b or b in 1 ) by ORDINAL1:14;

suppose 1 in b ; :: thesis: b -leading_coeff 1 = 1

hence b -leading_coeff 1 = 1 by Th55; :: thesis: verum

end;

suppose 1 = b ; :: thesis: b -leading_coeff 1 = 1

hence b -leading_coeff 1 = 1 by Th53; :: thesis: verum

end;

suppose b in 1 ; :: thesis: b -leading_coeff 1 = 1

then b = 0 by TARSKI:def 1, CARD_1:49;
hence b -leading_coeff 1 = 1 by Th52; :: thesis: verum

end;

end;