let R be Ring; :: thesis: Char R = min* (CharSet R)
set n = Char R;

per cases ( Char R = 0 or Char R > 0 ) ;

suppose A1: Char R = 0 ; :: thesis: Char R = min* (CharSet R)

then CharSet R = {} by Th77;
hence Char R = min* (CharSet R) by A1, NAT_1:def 1; :: thesis: verum

end;

suppose Char R > 0 ; :: thesis: Char R = min* (CharSet R)

then reconsider n1 = Char R as positive Nat ;
reconsider R1 = R as n1 -characteristic Ring by Def6;
A2: ( Char R = Char R1 & Char R1 = min (CharSet R1) ) by Th78;
then A3: Char R in CharSet R by XXREAL_2:def 7;
for k being Nat st k in CharSet R holds
Char R <= k by A2, XXREAL_2:def 7;
hence Char R = min* (CharSet R) by A3, NAT_1:def 1; :: thesis: verum

end;

end;