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: ( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper )

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

suppose J = {(0. F)} ; :: thesis: ( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper )

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

end;

suppose J = the carrier of F ; :: thesis: ( not {(0. F)} -Ideal c= J or J = {(0. F)} -Ideal or not J is proper )

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

end;

end;

end;

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