for n being positive Nat holds n '*' (1. INT.Ring) <> 0. INT.Ring by Lm8;
hence Char INT.Ring = 0 by Def5; :: thesis: verum