let A be non degenerated commutative Ring; :: thesis: 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; :: thesis: 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; :: thesis: ( not p c= q or q = p or not q is proper )
assume A7: p c= q ; :: thesis: ( q = p or not q is proper )
per cases ( q is proper or not q is proper ) ;
suppose A8: q is proper ; :: thesis: ( q = p or not q is proper )
A9: multClSet (J,(1. A)) = {(1. A)} by Lm6;
A10: q /\ (multClSet (J,(1. A))) = {}
proof
assume q /\ (multClSet (J,(1. A))) <> {} ; :: thesis: contradiction
then consider y being object such that
A12: y in q /\ (multClSet (J,(1. A))) by XBOOLE_0:def 1;
A13: ( y in q & y in multClSet (J,(1. A)) ) by A12, XBOOLE_0:def 4;
1. A in q by A9, A13, TARSKI:def 1;
hence contradiction by A8, IDEAL_1:19; :: thesis: verum
end;
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; :: thesis: verum
end;
suppose not q is proper ; :: thesis: ( q = p or not q is proper )
hence ( q = p or not q is proper ) ; :: thesis: verum
end;
end;
end;
then p is quasi-maximal ;
hence ex m being maximal Ideal of A st J c= m by A5, A6; :: thesis: verum