let F be Field; :: thesis: F is PID
let I be Ideal of F; :: according to IDEAL_1:def 28 :: thesis: I is principal

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

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

then I = {(0. F)} -Ideal by IDEAL_1:47;
hence I is principal ; :: thesis: verum

end;

suppose I = the carrier of F ; :: thesis: I is principal

then I = {(1. F)} -Ideal by IDEAL_1:51;
hence I is principal ; :: thesis: verum

end;

end;