Char R = n by Def6;
then ( n '*' (1. R) = 0. R & n <> 0 & ( for m being positive Nat st m < n holds
m '*' (1. R) <> 0. R ) ) by Def5;
then n in { k where k is positive Nat : k '*' (1. R) = 0. R } ;
hence not CharSet R is empty ; :: thesis: verum