theorem degen: :: FIELD_6:1

for R being Ring holds
( R is degenerated iff the carrier of R = {(0. R)} )