set I = {(0. F)} -Ideal ;
{(0. F)} -Ideal = {(0. F)} by IDEAL_1:47;
then not 1. F in {(0. F)} -Ideal by TARSKI:def 1;
then A: {(0. F)} -Ideal is proper by IDEAL_1:19;
for J being Ideal of F holds
( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper )

proof

let J be Ideal of F; :: thesis:

per cases by IDEAL_1:22;

suppose J = {(0. F)} ; :: thesis:

hence ( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper ) by IDEAL_1:47; :: thesis:

end;

suppose J = the carrier of F ; :: thesis:

then J = [#] F ;
hence ( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper ) ; :: thesis:

end;

end;

end;

hence {(0. F)} -Ideal is maximal by A, RING_1:def 3, RING_1:def 4; :: thesis: