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

A1: now :: thesis: ( R is Field implies for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) )

assume A2: R is Field ; :: thesis: for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R )
thus for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) :: thesis: verum

proof

let I be Ideal of R; :: thesis: ( I = {(0. R)} or I = the carrier of R )
assume A3: I <> {(0. R)} ; :: thesis: I = the carrier of R
reconsider R = R as Field by A2;
ex a being Element of R st
( a in I & a <> 0. R )

proof

assume A4: for a being Element of R holds
( not a in I or not a <> 0. R ) ; :: thesis: contradiction

A5: now :: thesis: for u being object st u in I holds
u in {(0. R)}

let u be object ; :: thesis: ( u in I implies u in {(0. R)} )
assume u in I ; :: thesis: u in {(0. R)}
then reconsider u9 = u as Element of I ;
u9 = 0. R by A4;
hence u in {(0. R)} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for u being object st u in {(0. R)} holds
u in I

let u be object ; :: thesis: ( u in {(0. R)} implies u in I )
assume A6: u in {(0. R)} ; :: thesis: u in I
then reconsider u9 = u as Element of R ;
u9 = 0. R by A6, TARSKI:def 1;
hence u in I by Th3; :: thesis: verum

end;

hence contradiction by A3, A5, TARSKI:2; :: thesis: verum

end;

then consider a being Element of R such that
A7: a in I and
A8: a <> 0. R ;
ex b being Element of R st b * a = 1. R by A8, VECTSP_1:def 9;
then 1. R in I by A7, Def3;
then not I is proper by Th19;
hence I = the carrier of R by SUBSET_1:def 6; :: thesis: verum

end;

end;

now :: thesis: ( ( for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) ) implies R is Field )

assume A9: for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) ; :: thesis: R is Field

now :: thesis: for a being Element of R st a <> 0. R holds
ex b being Element of R st b * a = 1. R

let a be Element of R; :: thesis: ( a <> 0. R implies ex b being Element of R st b * a = 1. R )
reconsider a9 = a as Element of R ;
reconsider M = { (a9 * r) where r is Element of R : verum } as Ideal of R by Lm1;
a * (1. R) = a ;
then A10: a in M ;
assume a <> 0. R ; :: thesis: ex b being Element of R st b * a = 1. R
then M <> {(0. R)} by A10, TARSKI:def 1;
then M = the carrier of R by A9;
then 1. R in M ;
then ex b being Element of R st a * b = 1. R ;
hence ex b being Element of R st b * a = 1. R ; :: thesis: verum

end;

hence R is Field by VECTSP_1:def 9; :: thesis: verum

end;

hence ( R is Field iff for I being Ideal of R holds
( I = {(0. R)} or I = the carrier of R ) ) by A1; :: thesis: verum