let n be positive Nat; :: thesis: for R being n -characteristic Ring holds Char R = min (CharSet R)
let R be n -characteristic Ring; :: thesis: Char R = min (CharSet R)
set M = CharSet R;
A1: n = Char R by Def6;
( n '*' (1. R) = 0. R & n <> 0 & ( for m being positive Nat st m < n holds
m '*' (1. R) <> 0. R ) ) by A1, Def5;
then A2: n in CharSet R ;
now :: thesis: for x being ExtReal st x in CharSet R holds
n <= x
let x be ExtReal; :: thesis: ( x in CharSet R implies n <= x )
assume x in CharSet R ; :: thesis: n <= x
then consider m being positive Nat such that
A3: ( x = m & m '*' (1. R) = 0. R ) ;
thus n <= x by A3, A1, Def5; :: thesis: verum
end;
hence Char R = min (CharSet R) by A2, A1, XXREAL_2:def 7; :: thesis: verum