let A be non degenerated commutative Ring; :: thesis: ( A is Field implies Ideals A = {{(0. A)}, the carrier of A} )
assume A1: A is Field ; :: thesis: Ideals A = {{(0. A)}, the carrier of A}
A2: for x being object st x in Ideals A holds
x in {{(0. A)}, the carrier of A}

proof

let x be object ; :: thesis: ( x in Ideals A implies x in {{(0. A)}, the carrier of A} )
assume x in Ideals A ; :: thesis: x in {{(0. A)}, the carrier of A}
then x in { I where I is Ideal of A : verum } by RING_2:def 3;
then consider x1 being Ideal of A such that
A4: x1 = x ;
( x = {(0. A)} or x = the carrier of A ) by A1, A4, IDEAL_1:22;
hence x in {{(0. A)}, the carrier of A} by TARSKI:def 2; :: thesis: verum

end;

for x being object st x in {{(0. A)}, the carrier of A} holds
x in Ideals A

proof

let x be object ; :: thesis: ( x in {{(0. A)}, the carrier of A} implies x in Ideals A )
assume x in {{(0. A)}, the carrier of A} ; :: thesis: x in Ideals A

per cases then ( x = {(0. A)} or x = the carrier of A ) by TARSKI:def 2;

suppose x = {(0. A)} ; :: thesis: x in Ideals A

then x in { I where I is Ideal of A : verum } ;
hence x in Ideals A by RING_2:def 3; :: thesis: verum

end;

suppose x = the carrier of A ; :: thesis: x in Ideals A

then x is Ideal of A by IDEAL_1:10;
then x in { I where I is Ideal of A : verum } ;
hence x in Ideals A by RING_2:def 3; :: thesis: verum

end;

end;

end;

hence Ideals A = {{(0. A)}, the carrier of A} by A2, TARSKI:2; :: thesis: verum