theorem :: IDEAL_1:22

for R being non degenerated comRing holds
( R is Field iff for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) )