let A be non degenerated commutative Ring; :: thesis:
assume A1: A is Field ; :: thesis:
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:
assume x in Ideals A ; :: thesis:
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:

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:
assume x in {{(0. A)}, the carrier of A} ; :: thesis:

per cases by TARSKI:def 2;

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

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

end;

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

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:

end;

end;

end;

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