let F be Field; :: thesis: F is Noetherian
let I be Ideal of F; :: according to IDEAL_1:def 26 :: thesis: I is finitely_generated

per cases ( I = {(0. F)} or I = the carrier of F ) by IDEAL_1:22;

suppose A1: I = {(0. F)} ; :: thesis: I is finitely_generated

reconsider s0F = {(0. F)} as non empty finite Subset of F ;
{(0. F)} = s0F -Ideal by IDEAL_1:47;
hence I is finitely_generated by A1; :: thesis: verum

end;

suppose A2: I = the carrier of F ; :: thesis: I is finitely_generated

reconsider s1F = {(1_ F)} as non empty finite Subset of F ;
the carrier of F = s1F -Ideal by IDEAL_1:51;
hence I is finitely_generated by A2; :: thesis: verum

end;

end;