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;