let A be non degenerated commutative Ring; :: thesis:
let J be proper Ideal of A; :: thesis:
let f be Element of A; :: thesis:
assume A1: not f in sqrt J ; :: thesis:
set S = Ideals (A,J,f);
set P = RelIncl (Ideals (A,J,f));
A2: field (RelIncl (Ideals (A,J,f))) = Ideals (A,J,f) by WELLORD2:def 1;
for Y being set st Y c= Ideals (A,J,f) & (RelIncl (Ideals (A,J,f))) |_2 Y is being_linear-order holds
ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )

take x = J; :: thesis:
thus ( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) ) by A5, A1, Th7; :: thesis:

end;

then consider e being object such that
A6: e in Y ;
take x = union Y; :: thesis:
for a being object st a in x holds
a in the carrier of A

let a be object ; :: thesis:
assume a in x ; :: thesis:
then consider Z being set such that
A7: a in Z and
A8: Z in Y by TARSKI:def 4;
Z in Ideals (A,J,f) by A3, A8;
then ex A1 being Subset of A st
( Z = A1 & A1 is proper Ideal of A & J c= A1 & A1 /\ (multClSet (J,f)) = {} ) ;
hence a in the carrier of A by A7; :: thesis:

end;

then x c= the carrier of A ;
then reconsider B = x as Subset of A ;
A9: B is left-ideal

let p, a be Element of A; :: according to IDEAL_1:def 2 :: thesis:
assume a in B ; :: thesis:
then consider Aa being set such that
A10: a in Aa and
A11: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A11;
then consider Ia being Subset of A such that
A12: Aa = Ia and
A13: Ia is proper Ideal of A and
J c= Ia and
Ia /\ (multClSet (J,f)) = {} ;
( p * a in Ia & Ia c= B ) by A10, A11, A12, A13, IDEAL_1:def 2, ZFMISC_1:74;
hence p * a in B ; :: thesis:

end;

assume not B is proper ; :: thesis:
then consider Aa being set such that
A16: 1. A in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A17;
then ex Ia being Subset of A st
( Aa = Ia & Ia is proper Ideal of A & J c= Ia & Ia /\ (multClSet (J,f)) = {} ) ;
hence contradiction by A16, IDEAL_1:19; :: thesis:

end;

A19: field ((RelIncl (Ideals (A,J,f))) |_2 Y) = Y by A2, A3, ORDERS_1:71;
let a, b be Element of A; :: according to IDEAL_1:def 1 :: thesis:

end;

assume a in B ; :: thesis:
then consider Aa being set such that
A22: a in Aa and
A23: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A23;
then A24: ex Ia being Subset of A st
( Aa = Ia & Ia is proper Ideal of A & J c= Ia & Ia /\ (multClSet (J,f)) = {} ) ;
assume b in B ; :: thesis:
then consider Ab being set such that
A25: b in Ab and
A26: Ab in Y by TARSKI:def 4;
( [Aa,Ab] in (RelIncl (Ideals (A,J,f))) |_2 Y or [Ab,Aa] in (RelIncl (Ideals (A,J,f))) |_2 Y or Aa = Ab ) by A4, A23, A26, A19, RELAT_2:def 6, RELAT_2:def 14;
then ( [Aa,Ab] in RelIncl (Ideals (A,J,f)) or [Ab,Aa] in RelIncl (Ideals (A,J,f)) or Aa = Ab ) by XBOOLE_0:def 4;
then A27: ( Aa c= Ab or Ab c= Aa ) by A3, A23, A26, WELLORD2:def 1;
Ab in Ideals (A,J,f) by A3, A26;
then ex Ib being Subset of A st
( Ab = Ib & Ib is proper Ideal of A & J c= Ib & Ib /\ (multClSet (J,f)) = {} ) ;
hence a + b in B by A22, A23, A25, A26, A20, A24, A27; :: thesis:

end;

assume B /\ (multClSet (J,f)) <> {} ; :: thesis:
then consider y being object such that
A35: y in B /\ (multClSet (J,f)) by XBOOLE_0:def 1;
( y in B & y in multClSet (J,f) ) by A35, XBOOLE_0:def 4;
then consider Aa being set such that
A36: y in Aa and
A37: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A37;
then consider Ia being Subset of A such that
A38: Aa = Ia and
( Ia is proper Ideal of A & J c= Ia ) and
A39: Ia /\ (multClSet (J,f)) = {} ;
y in multClSet (J,f) by A35, XBOOLE_0:def 4;
hence contradiction by A39, A38, A36, XBOOLE_0:def 4; :: thesis:

end;

end;