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;