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

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

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

end;

now

let u be set ; :: thesis: ( u in {(0. R)} implies u in I )
assume A6: u in {(0. R)} ; :: thesis: u in I
then reconsider u' = u as Element of R ;
u' = 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 & a <> 0. R ) ;
consider b being Element of R such that
A8: b * a = 1. R by A7, VECTSP_1:def 20;
1. R in I by A7, A8, Def3;
then not I is proper by Th19;
hence I = the carrier of R by SUBSET_1:def 7; :: thesis: verum

end;

end;

now

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

now

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

end;

hence R is Field by VECTSP_1:def 20; :: 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