let R be Ring; :: thesis: ( Char R = 0 iff CharSet R = {} )

A1: now :: thesis: ( Char R = 0 implies CharSet R = {} )

assume A2: Char R = 0 ; :: thesis: CharSet R = {}

now :: thesis: for x being object holds not x in CharSet R

let x be object ; :: thesis: not x in CharSet R
assume x in CharSet R ; :: thesis: contradiction
then ex n being positive Nat st
( x = n & n '*' (1. R) = 0. R ) ;
hence contradiction by A2, Def5; :: thesis: verum

end;

hence CharSet R = {} by XBOOLE_0:def 1; :: thesis: verum

end;

now :: thesis: ( CharSet R = {} implies Char R = 0 )

assume A3: CharSet R = {} ; :: thesis: Char R = 0

now :: thesis: for m being positive Nat holds not m '*' (1. R) = 0. R

assume ex m being positive Nat st m '*' (1. R) = 0. R ; :: thesis: contradiction
then consider m being positive Nat such that
A4: m '*' (1. R) = 0. R ;
m in { k where k is positive Nat : k '*' (1. R) = 0. R } by A4;
hence contradiction by A3; :: thesis: verum

end;

hence Char R = 0 by Def5; :: thesis: verum

end;

hence ( Char R = 0 iff CharSet R = {} ) by A1; :: thesis: verum