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 } partially_orders { A where A is Ideal of R : A is proper }

proof

thus RelIncl { A where A is Ideal of R : A is proper } is_reflexive_in { A where A is Ideal of R : A is proper } by WELLORD2:29; :: according to ORDERS_1:def 7 :: thesis: ( RelIncl { A where A is Ideal of R : A is proper } is_transitive_in { A where A is Ideal of R : A is proper } & RelIncl { A where A is Ideal of R : A is proper } is_antisymmetric_in { A where A is Ideal of R : A is proper } )
thus 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:30; :: thesis: RelIncl { A where A is Ideal of R : A is proper } is_antisymmetric_in { A where A is Ideal of R : A is proper }
thus 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:31; :: thesis: verum

end;

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;
{ 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 9 :: 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
A3: Y c= { A where A is Ideal of R : A is proper } and
A4: (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 A5: 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

assume not x is proper ; :: thesis: contradiction
then A6: x = the carrier of R by SUBSET_1:def 7;
x = {(0. R)} by IDEAL_1:47;
then 1. R = 0. R by A6, 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 A5; :: 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 set such that
A7: e in Y by XBOOLE_0:def 1;
e in { A where A is Ideal of R : A is proper } by A3, A7;
then consider A being Ideal of R such that
A8: e = A and
A is proper ;
consider q being set such that
A9: q in A by XBOOLE_0:def 1;
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 set ; :: 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
A10: a in Z and
A11: Z in Y by TARSKI:def 4;
Z in { A where A is Ideal of R : A is proper } by A3, A11;
then ex A being Ideal of R st
( Z = A & A is proper ) ;
hence a in the carrier of R by A10; :: thesis: verum

end;

then reconsider B = x as Subset of R ;
A12: not B is empty by A7, A8, A9, TARSKI:def 4;
A13: B is add-closed

proof

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 )
assume a in B ; :: thesis: ( not b in B or a + b in B )
then consider Aa being set such that
A14: a in Aa and
A15: Aa in Y by TARSKI:def 4;
assume b in B ; :: thesis: a + b in B
then consider Ab being set such that
A16: b in Ab and
A17: Ab in Y by TARSKI:def 4;

A18: now

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 A19: a + b in A by IDEAL_1:def 1;
assume A in Y ; :: thesis: a + b in B
hence a + b in B by A19, TARSKI:def 4; :: thesis: verum

end;

Aa in { A where A is Ideal of R : A is proper } by A3, A15;
then consider Ia being Ideal of R such that
A20: Aa = Ia and
Ia is proper ;
Ab in { A where A is Ideal of R : A is proper } by A3, A17;
then consider Ib being Ideal of R such that
A21: Ab = Ib and
Ib is proper ;
(RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y is connected by A4, ORDERS_1:def 5;
then A22: (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;
RelIncl { A where A is Ideal of R : A is proper } is reflexive

proof

thus RelIncl { A where A is Ideal of R : A is proper } is_reflexive_in field (RelIncl { A where A is Ideal of R : A is proper } ) by A2, WELLORD2:29; :: according to RELAT_2:def 9 :: thesis: verum

end;

then field ((RelIncl { A where A is Ideal of R : A is proper } ) |_2 Y) = Y by A2, A3, ORDERS_1:181;
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 A15, A17, A22, 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 ( Aa c= Ab or Ab c= Aa ) by A3, A15, A17, WELLORD2:def 1;
hence a + b in B by A14, A15, A16, A17, A18, A20, A21; :: thesis: verum

end;

A23: 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
A24: a in Aa and
A25: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A3, A25;
then consider Ia being Ideal of R such that
A26: Aa = Ia and
Ia is proper ;
A27: p * a in Ia by A24, A26, IDEAL_1:def 2;
Ia c= B by A25, A26, ZFMISC_1:92;
hence p * a in B by A27; :: thesis: verum

end;

A28: 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
A29: a in Aa and
A30: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : A is proper } by A3, A30;
then consider Ia being Ideal of R such that
A31: Aa = Ia and
Ia is proper ;
A32: a * p in Ia by A29, A31, IDEAL_1:def 3;
Ia c= B by A30, A31, ZFMISC_1:92;
hence a * p in B by A32; :: thesis: verum

end;

now

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

end;

hence A35: x in { A where A is Ideal of R : A is proper } by A12, A13, A23, A28; :: 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 A36: 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:92;
hence [y,x] in RelIncl { A where A is Ideal of R : A is proper } by A3, A35, A36, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

then consider x being set such that
A37: x is_maximal_in RelIncl { A where A is Ideal of R : A is proper } by A1, A2, ORDERS_1:173;
A38: x in field (RelIncl { A where A is Ideal of R : A is proper } ) by A37, ORDERS_1:def 11;
then consider I being Ideal of R such that
A39: x = I and
A40: I is proper by A2;
take I ; :: thesis: I is maximal
thus I is proper by A40; :: 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 A41: I c= J ; :: thesis: ( J = I or not J is proper )

now

assume J is proper ; :: thesis: I = J
then A42: 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, A38, A39, A41, WELLORD2:def 1;
hence I = J by A2, A37, A39, A42, ORDERS_1:def 11; :: thesis: verum

end;

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