set S = { A where A is Ideal of R : A is proper } ;
set P = RelIncl { A where A is Ideal of R : A is proper } ;
A1: RelIncl { A where A is Ideal of R : A is proper } is_antisymmetric_in { A where A is Ideal of R : A is proper } by WELLORD2:21;
A2: field (RelIncl { A where A is Ideal of R : A is proper } ) = { A where A is Ideal of R : A is proper } by WELLORD2:def 1;
A3: { A where A is Ideal of R : A is proper } has_upper_Zorn_property_wrt RelIncl { A where A is Ideal of R : A is proper }

proof

let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( not Y c= { A where A is Ideal of R : A is proper } or not (RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y is being_linear-order or ex b₁ being set st
( b₁ in { A where A is Ideal of R : A is proper } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in RelIncl { A where A is Ideal of R : A is proper } ) ) ) )
assume that
A4: Y c= { A where A is Ideal of R : A is proper } and
A5: (RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y is being_linear-order ; :: thesis: ex b₁ being set st
( b₁ in { A where A is Ideal of R : A is proper } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

per cases ( Y is empty or not Y is empty ) ;

suppose A6: Y is empty ; :: thesis: ex b₁ being set st
( b₁ in { A where A is Ideal of R : A is proper } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

take x = {(0. R)} -Ideal ; :: thesis: ( x in { A where A is Ideal of R : A is proper } & ( for b₁ being set holds
( not b₁ in Y or [b₁,x] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

now :: thesis: x is proper

assume not x is proper ; :: thesis: contradiction
then A7: x = the carrier of R by SUBSET_1:def 6;
x = {(0. R)} by IDEAL_1:47;
then 1. R = 0. R by A7, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

hence x in { A where A is Ideal of R : A is proper } ; :: thesis: for b₁ being set holds
( not b₁ in Y or [b₁,x] in RelIncl { A where A is Ideal of R : A is proper } )
thus for b₁ being set holds
( not b₁ in Y or [b₁,x] in RelIncl { A where A is Ideal of R : A is proper } ) by A6; :: thesis: verum

end;

suppose not Y is empty ; :: thesis: ex b₁ being set st
( b₁ in { A where A is Ideal of R : A is proper } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

then consider e being object such that
A8: e in Y ;
take x = union Y; :: thesis: ( x in { A where A is Ideal of R : A is proper } & ( for b₁ being set holds
( not b₁ in Y or [b₁,x] in RelIncl { A where A is Ideal of R : A is proper } ) ) )
x c= the carrier of R

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in the carrier of R )
assume a in x ; :: thesis: a in the carrier of R
then consider Z being set such that
A9: a in Z and
A10: Z in Y by TARSKI:def 4;
Z in { A where A is Ideal of R : A is proper } by A4, A10;
then ex A being Ideal of R st
( Z = A & A is proper ) ;
hence a in the carrier of R by A9; :: thesis: verum

end;

then reconsider B = x as Subset of R ;
A11: B is right-ideal

proof

let p, a be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not a in B or a * p in B )
assume a in B ; :: thesis: a * p in B
then consider Aa being set such that
A12: a in Aa and
A13: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A4, A13;
then consider Ia being Ideal of R such that
A14: Aa = Ia and
Ia is proper ;
( a * p in Ia & Ia c= B ) by A12, A13, A14, IDEAL_1:def 3, ZFMISC_1:74;
hence a * p in B ; :: thesis: verum

end;

A15: B is left-ideal

proof

let p, a be Element of R; :: according to IDEAL_1:def 2 :: thesis: ( not a in B or p * a in B )
assume a in B ; :: thesis: p * a in B
then consider Aa being set such that
A16: a in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A4, A17;
then consider Ia being Ideal of R such that
A18: Aa = Ia and
Ia is proper ;
( p * a in Ia & Ia c= B ) by A16, A17, A18, IDEAL_1:def 2, ZFMISC_1:74;
hence p * a in B ; :: thesis: verum

end;

A19: now :: thesis: B is proper

assume not B is proper ; :: thesis: contradiction
then 1. R in B by A15, IDEAL_1:19;
then consider Aa being set such that
A20: 1. R in Aa and
A21: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A4, A21;
then ex Ia being Ideal of R st
( Aa = Ia & Ia is proper ) ;
hence contradiction by A20, IDEAL_1:19; :: thesis: verum

end;

A22: B is add-closed

proof

A23: field ((RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y) = Y by A2, A4, ORDERS_1:71;
let a, b be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not a in B or not b in B or a + b in B )

A24: now :: thesis: for A being Ideal of R st a in A & b in A & A in Y holds
a + b in B

let A be Ideal of R; :: thesis: ( a in A & b in A & A in Y implies a + b in B )
assume ( a in A & b in A ) ; :: thesis: ( A in Y implies a + b in B )
then A25: a + b in A by IDEAL_1:def 1;
assume A in Y ; :: thesis: a + b in B
hence a + b in B by A25, TARSKI:def 4; :: thesis: verum

end;

assume a in B ; :: thesis: ( not b in B or a + b in B )
then consider Aa being set such that
A26: a in Aa and
A27: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A4, A27;
then A28: ex Ia being Ideal of R st
( Aa = Ia & Ia is proper ) ;
assume b in B ; :: thesis: a + b in B
then consider Ab being set such that
A29: b in Ab and
A30: Ab in Y by TARSKI:def 4;
(RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y is connected by A5;
then (RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y is_connected_in field ((RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y) by RELAT_2:def 14;
then ( [Aa,Ab] in (RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y or [Ab,Aa] in (RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y or Aa = Ab ) by A27, A30, A23, RELAT_2:def 6;
then ( [Aa,Ab] in RelIncl { A where A is Ideal of R : A is proper } or [Ab,Aa] in RelIncl { A where A is Ideal of R : A is proper } or Aa = Ab ) by XBOOLE_0:def 4;
then A31: ( Aa c= Ab or Ab c= Aa ) by A4, A27, A30, WELLORD2:def 1;
Ab in { A where A is Ideal of R : A is proper } by A4, A30;
then ex Ib being Ideal of R st
( Ab = Ib & Ib is proper ) ;
hence a + b in B by A26, A27, A29, A30, A24, A28, A31; :: thesis: verum

end;

e in { A where A is Ideal of R : A is proper } by A4, A8;
then consider A being Ideal of R such that
A32: e = A and
A is proper ;
ex q being object st q in A by XBOOLE_0:def 1;
then not B is empty by A8, A32, TARSKI:def 4;
hence A33: x in { A where A is Ideal of R : A is proper } by A22, A15, A11, A19; :: thesis: for b₁ being set holds
( not b₁ in Y or [b₁,x] in RelIncl { A where A is Ideal of R : A is proper } )
let y be set ; :: thesis: ( not y in Y or [y,x] in RelIncl { A where A is Ideal of R : A is proper } )
assume A34: y in Y ; :: thesis: [y,x] in RelIncl { A where A is Ideal of R : A is proper }
then y c= x by ZFMISC_1:74;
hence [y,x] in RelIncl { A where A is Ideal of R : A is proper } by A4, A33, A34, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

( RelIncl { A where A is Ideal of R : A is proper } is_reflexive_in { A where A is Ideal of R : A is proper } & RelIncl { A where A is Ideal of R : A is proper } is_transitive_in { A where A is Ideal of R : A is proper } ) by WELLORD2:19, WELLORD2:20;
then RelIncl { A where A is Ideal of R : A is proper } partially_orders { A where A is Ideal of R : A is proper } by A1;
then consider x being set such that
A35: x is_maximal_in RelIncl { A where A is Ideal of R : A is proper } by A2, A3, ORDERS_1:63;
A36: x in field (RelIncl { A where A is Ideal of R : A is proper } ) by A35;
then consider I being Ideal of R such that
A37: x = I and
A38: I is proper by A2;
take I ; :: thesis: I is maximal
thus I is proper by A38; :: according to RING_1:def 4 :: thesis: I is quasi-maximal
let J be Ideal of R; :: according to RING_1:def 3 :: thesis: ( not I c= J or J = I or not J is proper )
assume A39: I c= J ; :: thesis: ( J = I or not J is proper )

now :: thesis: ( J is proper implies I = J )

assume J is proper ; :: thesis: I = J
then A40: J in { A where A is Ideal of R : A is proper } ;
then [I,J] in RelIncl { A where A is Ideal of R : A is proper } by A2, A36, A37, A39, WELLORD2:def 1;
hence I = J by A2, A35, A37, A40; :: thesis: verum

end;

hence ( J = I or not J is proper ) ; :: thesis: verum