set I = {(0. R)} -Ideal ;
consider J being Ideal of R such that
H: ( J <> {(0. R)} & J <> the carrier of R ) by IDEAL_1:22;
A: {(0. R)} -Ideal c= J
proof
now :: thesis: for o being object st o in {(0. R)} -Ideal holds
o in J
let o be object ; :: thesis: ( o in {(0. R)} -Ideal implies o in J )
assume o in {(0. R)} -Ideal ; :: thesis: o in J
then o in {(0. R)} by IDEAL_1:47;
then o = 0. R by TARSKI:def 1;
hence o in J by IDEAL_1:2; :: thesis: verum
end;
hence {(0. R)} -Ideal c= J ; :: thesis: verum
end;
B: J is proper by H, SUBSET_1:def 6;
J <> {(0. R)} -Ideal by H, IDEAL_1:47;
hence not {(0. R)} -Ideal is maximal by A, B, RING_1:def 3; :: thesis: verum