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 }

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 )

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

( 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;
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_{1} being set st

( b_{1} in { A where A is Ideal of R : A is proper } & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] 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_{1} being set st

( b_{1} in { A where A is Ideal of R : A is proper } & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

end;( b

( not b

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

( b

( not b

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

end;

suppose A6:
Y is empty
; :: thesis: ex b_{1} being set st

( b_{1} in { A where A is Ideal of R : A is proper } & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

( b

( not b

take x = {(0. R)} -Ideal ; :: thesis: ( x in { A where A is Ideal of R : A is proper } & ( for b_{1} being set holds

( not b_{1} in Y or [b_{1},x] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

_{1} being set holds

( not b_{1} in Y or [b_{1},x] in RelIncl { A where A is Ideal of R : A is proper } )

thus for b_{1} being set holds

( not b_{1} in Y or [b_{1},x] in RelIncl { A where A is Ideal of R : A is proper } )
by A6; :: thesis: verum

end;( not b

now :: thesis: x is proper

hence
x in { A where A is Ideal of R : A is proper }
; :: thesis: for bassume
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;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

( not b

thus for b

( not b

suppose
not Y is empty
; :: thesis: ex b_{1} being set st

( b_{1} in { A where A is Ideal of R : A is proper } & ( for b_{2} being set holds

( not b_{2} in Y or [b_{2},b_{1}] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

( b

( not b

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_{1} being set holds

( not b_{1} in Y or [b_{1},x] in RelIncl { A where A is Ideal of R : A is proper } ) ) )

x c= the carrier of R

A11: B is right-ideal

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_{1} being set holds

( not b_{1} in Y or [b_{1},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;A8: e in Y ;

take x = union Y; :: thesis: ( x in { A where A is Ideal of R : A is proper } & ( for b

( not b

x c= the carrier of R

proof

then reconsider B = x as Subset of R ;
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;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

A11: B is right-ideal

proof

A15:
B is left-ideal
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;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

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;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

A19: now :: thesis: B is proper

A22:
B is add-closed
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;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

proof

e in { A where A is Ideal of R : A is proper }
by A4, A8;
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 )

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;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

assume
a in B
; :: thesis: ( not b in B or a + b in B )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 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

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

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

( not b

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

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 )

hence
( J = I or not J is proper )
; :: thesis: verumassume
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;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