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