let A be non degenerated commutative Ring; for J being proper Ideal of A ex m being maximal Ideal of A st J c= m
let J be proper Ideal of A; ex m being maximal Ideal of A st J c= m
A1:
not 1. A in sqrt J
by Lm5;
set S = Ideals (A,J,(1. A));
set P = RelIncl (Ideals (A,J,(1. A)));
A2:
field (RelIncl (Ideals (A,J,(1. A)))) = Ideals (A,J,(1. A))
by WELLORD2:def 1;
RelIncl (Ideals (A,J,(1. A))) partially_orders Ideals (A,J,(1. A))
by WELLORD2:19, WELLORD2:20, WELLORD2:21;
then consider I being set such that
A3:
I is_maximal_in RelIncl (Ideals (A,J,(1. A)))
by A1, A2, Th8, ORDERS_1:63;
I in Ideals (A,J,(1. A))
by WELLORD2:def 1, A3;
then consider p being Subset of A such that
A4:
p = I
and
A5:
p is proper Ideal of A
and
A6:
J c= p
and
p /\ (multClSet (J,(1. A))) = {}
;
for q being Ideal of A holds
( not p c= q or q = p or not q is proper )
proof
let q be
Ideal of
A;
( not p c= q or q = p or not q is proper )
assume A7:
p c= q
;
( q = p or not q is proper )
per cases
( q is proper or not q is proper )
;
suppose A8:
q is
proper
;
( q = p or not q is proper )A9:
multClSet (
J,
(1. A))
= {(1. A)}
by Lm6;
A10:
q /\ (multClSet (J,(1. A))) = {}
J c= q
by A6, A7;
then A14:
q in Ideals (
A,
J,
(1. A))
by A8, A10;
[p,q] in RelIncl (Ideals (A,J,(1. A)))
by A2, A3, A4, A7, A14, WELLORD2:def 1;
hence
(
q = p or not
q is
proper )
by A2, A3, A4, A14;
verum end; end;
end;
then
p is quasi-maximal
;
hence
ex m being maximal Ideal of A st J c= m
by A5, A6; verum