let R be Ring; :: thesis: ( Char R = 0 implies R is infinite )
assume Char R = 0 ; :: thesis: R is infinite
then R is 0 -characteristic by RING_3:def 6;
hence R is infinite ; :: thesis: verum