:: WAYBEL_7 semantic presentation begin theorem Th1: :: WAYBEL_7:1 for L being complete LATTICE for X, Y being set st X c= Y holds ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) proof let L be complete LATTICE; ::_thesis: for X, Y being set st X c= Y holds ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) let X, Y be set ; ::_thesis: ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) ) A1: ( ex_inf_of X,L & ex_inf_of Y,L ) by YELLOW_0:17; ( ex_sup_of X,L & ex_sup_of Y,L ) by YELLOW_0:17; hence ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) ) by A1, YELLOW_0:34, YELLOW_0:35; ::_thesis: verum end; theorem Th2: :: WAYBEL_7:2 for X being set holds the carrier of (BoolePoset X) = bool X proof let X be set ; ::_thesis: the carrier of (BoolePoset X) = bool X set L = BoolePoset X; BoolePoset X = InclPoset (bool X) by YELLOW_1:4; then BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1; hence the carrier of (BoolePoset X) = bool X ; ::_thesis: verum end; theorem Th3: :: WAYBEL_7:3 for L being non empty antisymmetric bounded RelStr holds ( L is trivial iff Top L = Bottom L ) proof let L be non empty antisymmetric bounded RelStr ; ::_thesis: ( L is trivial iff Top L = Bottom L ) thus ( L is trivial implies Top L = Bottom L ) by STRUCT_0:def_10; ::_thesis: ( Top L = Bottom L implies L is trivial ) assume A1: Top L = Bottom L ; ::_thesis: L is trivial let x, y be Element of L; :: according to STRUCT_0:def_10 ::_thesis: x = y reconsider x = x, y = y as Element of L ; ( x >= Bottom L & x <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45; then A2: x = Bottom L by ORDERS_2:2; ( y >= Bottom L & y <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45; hence x = y by A2, ORDERS_2:2; ::_thesis: verum end; registration let X be set ; cluster BoolePoset X -> Boolean ; coherence BoolePoset X is Boolean ; end; registration let X be non empty set ; cluster BoolePoset X -> non trivial ; coherence not BoolePoset X is trivial proof ( Top (BoolePoset X) = X & Bottom (BoolePoset X) = {} ) by YELLOW_1:18, YELLOW_1:19; hence not BoolePoset X is trivial by Th3; ::_thesis: verum end; end; theorem Th4: :: WAYBEL_7:4 for L being non empty lower-bounded Poset for F being Filter of L holds ( F is proper iff not Bottom L in F ) proof let L be non empty lower-bounded Poset; ::_thesis: for F being Filter of L holds ( F is proper iff not Bottom L in F ) let F be Filter of L; ::_thesis: ( F is proper iff not Bottom L in F ) hereby ::_thesis: ( not Bottom L in F implies F is proper ) assume F is proper ; ::_thesis: not Bottom L in F then F <> the carrier of L by SUBSET_1:def_6; then consider a being set such that A1: ( ( a in F & not a in the carrier of L ) or ( a in the carrier of L & not a in F ) ) by TARSKI:1; reconsider a = a as Element of L by A1; a >= Bottom L by YELLOW_0:44; hence not Bottom L in F by A1, WAYBEL_0:def_20; ::_thesis: verum end; assume not Bottom L in F ; ::_thesis: F is proper then F <> the carrier of L ; hence F is proper by SUBSET_1:def_6; ::_thesis: verum end; registration cluster non empty non trivial strict reflexive transitive antisymmetric Boolean non void with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( not b1 is trivial & b1 is Boolean & b1 is strict ) proof take BoolePoset {{}} ; ::_thesis: ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict ) thus ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict ) ; ::_thesis: verum end; end; registration let L be non trivial upper-bounded Poset; cluster non empty proper filtered upper for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is proper proof take F = uparrow (Top L); ::_thesis: F is proper assume not F is proper ; ::_thesis: contradiction then A1: F = the carrier of L by SUBSET_1:def_6; now__::_thesis:_for_x,_y_being_Element_of_L_holds_x_=_y let x, y be Element of L; ::_thesis: x = y A2: F = {(Top L)} by WAYBEL_4:24; then x = Top L by A1, TARSKI:def_1; hence x = y by A1, A2, TARSKI:def_1; ::_thesis: verum end; hence contradiction by STRUCT_0:def_10; ::_thesis: verum end; end; theorem Th5: :: WAYBEL_7:5 for X being set for a being Element of (BoolePoset X) holds 'not' a = X \ a proof let X be set ; ::_thesis: for a being Element of (BoolePoset X) holds 'not' a = X \ a let a be Element of (BoolePoset X); ::_thesis: 'not' a = X \ a A1: the carrier of (BoolePoset X) = bool X by Th2; reconsider b = X \ a as Element of (BoolePoset X) by Th2; A2: a misses b by XBOOLE_1:79; A3: a "/\" b = a /\ b by YELLOW_1:17 .= {} by A2, XBOOLE_0:def_7 .= Bottom (BoolePoset X) by YELLOW_1:18 ; a "\/" b = a \/ b by YELLOW_1:17 .= X by A1, XBOOLE_1:45 .= Top (BoolePoset X) by YELLOW_1:19 ; then b is_a_complement_of a by A3, WAYBEL_1:def_23; hence 'not' a = X \ a by YELLOW_5:11; ::_thesis: verum end; theorem :: WAYBEL_7:6 for X being set for Y being Subset of (BoolePoset X) holds ( Y is lower iff for x, y being set st x c= y & y in Y holds x in Y ) proof let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds ( Y is lower iff for x, y being set st x c= y & y in Y holds x in Y ) let Y be Subset of (BoolePoset X); ::_thesis: ( Y is lower iff for x, y being set st x c= y & y in Y holds x in Y ) A1: the carrier of (BoolePoset X) = bool X by Th2; hereby ::_thesis: ( ( for x, y being set st x c= y & y in Y holds x in Y ) implies Y is lower ) assume A2: Y is lower ; ::_thesis: for x, y being set st x c= y & y in Y holds x in Y let x, y be set ; ::_thesis: ( x c= y & y in Y implies x in Y ) assume that A3: x c= y and A4: y in Y ; ::_thesis: x in Y reconsider a = x, b = y as Element of (BoolePoset X) by A1, A3, A4, XBOOLE_1:1; a <= b by A3, YELLOW_1:2; hence x in Y by A2, A4, WAYBEL_0:def_19; ::_thesis: verum end; assume A5: for x, y being set st x c= y & y in Y holds x in Y ; ::_thesis: Y is lower let a, b be Element of (BoolePoset X); :: according to WAYBEL_0:def_19 ::_thesis: ( not a in Y or not b <= a or b in Y ) assume that A6: a in Y and A7: b <= a ; ::_thesis: b in Y b c= a by A7, YELLOW_1:2; hence b in Y by A5, A6; ::_thesis: verum end; theorem Th7: :: WAYBEL_7:7 for X being set for Y being Subset of (BoolePoset X) holds ( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds y in Y ) proof let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds ( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds y in Y ) let Y be Subset of (BoolePoset X); ::_thesis: ( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds y in Y ) A1: the carrier of (BoolePoset X) = bool X by Th2; hereby ::_thesis: ( ( for x, y being set st x c= y & y c= X & x in Y holds y in Y ) implies Y is upper ) assume A2: Y is upper ; ::_thesis: for x, y being set st x c= y & y c= X & x in Y holds y in Y let x, y be set ; ::_thesis: ( x c= y & y c= X & x in Y implies y in Y ) assume that A3: x c= y and A4: y c= X and A5: x in Y ; ::_thesis: y in Y reconsider a = x, b = y as Element of (BoolePoset X) by A4, A5, Th2; a <= b by A3, YELLOW_1:2; hence y in Y by A2, A5, WAYBEL_0:def_20; ::_thesis: verum end; assume A6: for x, y being set st x c= y & y c= X & x in Y holds y in Y ; ::_thesis: Y is upper let a, b be Element of (BoolePoset X); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in Y or not a <= b or b in Y ) assume that A7: a in Y and A8: b >= a ; ::_thesis: b in Y a c= b by A8, YELLOW_1:2; hence b in Y by A1, A6, A7; ::_thesis: verum end; theorem :: WAYBEL_7:8 for X being set for Y being lower Subset of (BoolePoset X) holds ( Y is directed iff for x, y being set st x in Y & y in Y holds x \/ y in Y ) proof let X be set ; ::_thesis: for Y being lower Subset of (BoolePoset X) holds ( Y is directed iff for x, y being set st x in Y & y in Y holds x \/ y in Y ) let Y be lower Subset of (BoolePoset X); ::_thesis: ( Y is directed iff for x, y being set st x in Y & y in Y holds x \/ y in Y ) hereby ::_thesis: ( ( for x, y being set st x in Y & y in Y holds x \/ y in Y ) implies Y is directed ) assume A1: Y is directed ; ::_thesis: for x, y being set st x in Y & y in Y holds x \/ y in Y let x, y be set ; ::_thesis: ( x in Y & y in Y implies x \/ y in Y ) assume A2: ( x in Y & y in Y ) ; ::_thesis: x \/ y in Y then reconsider a = x, b = y as Element of (BoolePoset X) ; a "\/" b in Y by A1, A2, WAYBEL_0:40; hence x \/ y in Y by YELLOW_1:17; ::_thesis: verum end; assume A3: for x, y being set st x in Y & y in Y holds x \/ y in Y ; ::_thesis: Y is directed now__::_thesis:_for_a,_b_being_Element_of_(BoolePoset_X)_st_a_in_Y_&_b_in_Y_holds_ a_"\/"_b_in_Y let a, b be Element of (BoolePoset X); ::_thesis: ( a in Y & b in Y implies a "\/" b in Y ) assume ( a in Y & b in Y ) ; ::_thesis: a "\/" b in Y then a \/ b in Y by A3; hence a "\/" b in Y by YELLOW_1:17; ::_thesis: verum end; hence Y is directed by WAYBEL_0:40; ::_thesis: verum end; theorem Th9: :: WAYBEL_7:9 for X being set for Y being upper Subset of (BoolePoset X) holds ( Y is filtered iff for x, y being set st x in Y & y in Y holds x /\ y in Y ) proof let X be set ; ::_thesis: for Y being upper Subset of (BoolePoset X) holds ( Y is filtered iff for x, y being set st x in Y & y in Y holds x /\ y in Y ) let Y be upper Subset of (BoolePoset X); ::_thesis: ( Y is filtered iff for x, y being set st x in Y & y in Y holds x /\ y in Y ) hereby ::_thesis: ( ( for x, y being set st x in Y & y in Y holds x /\ y in Y ) implies Y is filtered ) assume A1: Y is filtered ; ::_thesis: for x, y being set st x in Y & y in Y holds x /\ y in Y let x, y be set ; ::_thesis: ( x in Y & y in Y implies x /\ y in Y ) assume A2: ( x in Y & y in Y ) ; ::_thesis: x /\ y in Y then reconsider a = x, b = y as Element of (BoolePoset X) ; a "/\" b in Y by A1, A2, WAYBEL_0:41; hence x /\ y in Y by YELLOW_1:17; ::_thesis: verum end; assume A3: for x, y being set st x in Y & y in Y holds x /\ y in Y ; ::_thesis: Y is filtered now__::_thesis:_for_a,_b_being_Element_of_(BoolePoset_X)_st_a_in_Y_&_b_in_Y_holds_ a_"/\"_b_in_Y let a, b be Element of (BoolePoset X); ::_thesis: ( a in Y & b in Y implies a "/\" b in Y ) assume ( a in Y & b in Y ) ; ::_thesis: a "/\" b in Y then a /\ b in Y by A3; hence a "/\" b in Y by YELLOW_1:17; ::_thesis: verum end; hence Y is filtered by WAYBEL_0:41; ::_thesis: verum end; theorem :: WAYBEL_7:10 for X being set for Y being non empty lower Subset of (BoolePoset X) holds ( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds union Z in Y ) proof let X be set ; ::_thesis: for Y being non empty lower Subset of (BoolePoset X) holds ( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds union Z in Y ) let Y be non empty lower Subset of (BoolePoset X); ::_thesis: ( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds union Z in Y ) hereby ::_thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds union Z in Y ) implies Y is directed ) assume A1: Y is directed ; ::_thesis: for Z being finite Subset-Family of X st Z c= Y holds union Z in Y let Z be finite Subset-Family of X; ::_thesis: ( Z c= Y implies union Z in Y ) reconsider B = Z as Subset of (BoolePoset X) by Th2; assume Z c= Y ; ::_thesis: union Z in Y then reconsider A = Z as finite Subset of Y ; A2: ( A <> {} implies sup B in Y ) by A1, WAYBEL_0:42; Bottom (BoolePoset X) in Y by A1, WAYBEL_4:21; hence union Z in Y by A2, YELLOW_1:18, YELLOW_1:21, ZFMISC_1:2; ::_thesis: verum end; assume A3: for Z being finite Subset-Family of X st Z c= Y holds union Z in Y ; ::_thesis: Y is directed A4: the carrier of (BoolePoset X) = bool X by Th2; now__::_thesis:_for_A_being_finite_Subset_of_Y_st_A_<>_{}_holds_ "\/"_(A,(BoolePoset_X))_in_Y let A be finite Subset of Y; ::_thesis: ( A <> {} implies "\/" (A,(BoolePoset X)) in Y ) reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1:1; assume A <> {} ; ::_thesis: "\/" (A,(BoolePoset X)) in Y reconsider Z = Z as finite Subset-Family of X ; A c= the carrier of (BoolePoset X) by XBOOLE_1:1; then union Z = "\/" (A,(BoolePoset X)) by YELLOW_1:21; hence "\/" (A,(BoolePoset X)) in Y by A3; ::_thesis: verum end; hence Y is directed by WAYBEL_0:42; ::_thesis: verum end; theorem Th11: :: WAYBEL_7:11 for X being set for Y being non empty upper Subset of (BoolePoset X) holds ( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y ) proof let X be set ; ::_thesis: for Y being non empty upper Subset of (BoolePoset X) holds ( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y ) let Y be non empty upper Subset of (BoolePoset X); ::_thesis: ( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y ) hereby ::_thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y ) implies Y is filtered ) assume A1: Y is filtered ; ::_thesis: for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y then Top (BoolePoset X) in Y by WAYBEL_4:22; then A2: X in Y by YELLOW_1:19; let Z be finite Subset-Family of X; ::_thesis: ( Z c= Y implies Intersect Z in Y ) reconsider B = Z as Subset of (BoolePoset X) by Th2; assume Z c= Y ; ::_thesis: Intersect Z in Y then reconsider A = Z as finite Subset of Y ; ( A <> {} implies ( inf B in Y & inf B = meet B ) ) by A1, WAYBEL_0:43, YELLOW_1:20; hence Intersect Z in Y by A2, SETFAM_1:def_9; ::_thesis: verum end; assume A3: for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y ; ::_thesis: Y is filtered A4: the carrier of (BoolePoset X) = bool X by Th2; now__::_thesis:_for_A_being_finite_Subset_of_Y_st_A_<>_{}_holds_ "/\"_(A,(BoolePoset_X))_in_Y let A be finite Subset of Y; ::_thesis: ( A <> {} implies "/\" (A,(BoolePoset X)) in Y ) reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1:1; assume A5: A <> {} ; ::_thesis: "/\" (A,(BoolePoset X)) in Y reconsider Z = Z as finite Subset-Family of X ; A c= the carrier of (BoolePoset X) by XBOOLE_1:1; then "/\" (A,(BoolePoset X)) = meet Z by A5, YELLOW_1:20 .= Intersect Z by A5, SETFAM_1:def_9 ; hence "/\" (A,(BoolePoset X)) in Y by A3; ::_thesis: verum end; hence Y is filtered by WAYBEL_0:43; ::_thesis: verum end; begin definition let L be with_infima Poset; let I be Ideal of L; attrI is prime means :Def1: :: WAYBEL_7:def 1 for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ); end; :: deftheorem Def1 defines prime WAYBEL_7:def_1_:_ for L being with_infima Poset for I being Ideal of L holds ( I is prime iff for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ) ); theorem Th12: :: WAYBEL_7:12 for L being with_infima Poset for I being Ideal of L holds ( I is prime iff for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) proof let L be with_infima Poset; ::_thesis: for I being Ideal of L holds ( I is prime iff for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) let I be Ideal of L; ::_thesis: ( I is prime iff for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) thus ( I is prime implies for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) ::_thesis: ( ( for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) implies I is prime ) proof defpred S1[ set ] means ( not $1 is empty & "/\" ($1,L) in I implies ex a being Element of L st ( a in $1 & a in I ) ); assume A1: for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) let A be non empty finite Subset of L; ::_thesis: ( inf A in I implies ex a being Element of L st ( a in A & a in I ) ) A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] ) assume that A3: x in A and A4: B c= A and A5: S1[B] ; ::_thesis: S1[B \/ {x}] thus S1[B \/ {x}] ::_thesis: verum proof reconsider a = x as Element of L by A3; reconsider C = B as finite Subset of L by A4, XBOOLE_1:1; assume that not B \/ {x} is empty and A6: "/\" ((B \/ {x}),L) in I ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) then ( "/\" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39; hence ex a being Element of L st ( a in B \/ {x} & a in I ) by A6; ::_thesis: verum end; supposeA7: B <> {} ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) A8: inf {a} = a by YELLOW_0:39; A9: ex_inf_of {a},L by YELLOW_0:55; ex_inf_of C,L by A7, YELLOW_0:55; then A10: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A9, YELLOW_2:4; hereby ::_thesis: verum percases ( inf C in I or a in I ) by A1, A6, A10, A8; suppose inf C in I ; ::_thesis: ex b being Element of L st ( b in B \/ {x} & b in I ) then consider b being Element of L such that A11: ( b in B & b in I ) by A5, A7; take b = b; ::_thesis: ( b in B \/ {x} & b in I ) thus ( b in B \/ {x} & b in I ) by A11, XBOOLE_0:def_3; ::_thesis: verum end; supposeA12: a in I ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) take a = a; ::_thesis: ( a in B \/ {x} & a in I ) a in {a} by TARSKI:def_1; hence ( a in B \/ {x} & a in I ) by A12, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; end; end; end; A13: S1[ {} ] ; A14: A is finite ; S1[A] from FINSET_1:sch_2(A14, A13, A2); hence ( inf A in I implies ex a being Element of L st ( a in A & a in I ) ) ; ::_thesis: verum end; assume A15: for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ; ::_thesis: I is prime let a, b be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not a "/\" b in I or a in I or b in I ) assume a "/\" b in I ; ::_thesis: ( a in I or b in I ) then inf {a,b} in I by YELLOW_0:40; then ex x being Element of L st ( x in {a,b} & x in I ) by A15; hence ( a in I or b in I ) by TARSKI:def_2; ::_thesis: verum end; registration let L be LATTICE; cluster non empty directed lower prime for Element of bool the carrier of L; existence ex b1 being Ideal of L st b1 is prime proof take [#] L ; ::_thesis: [#] L is prime let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in [#] L or x in [#] L or y in [#] L ) thus ( not x "/\" y in [#] L or x in [#] L or y in [#] L ) ; ::_thesis: verum end; end; theorem :: WAYBEL_7:13 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being set st x is prime Ideal of L1 holds x is prime Ideal of L2 proof let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being set st x is prime Ideal of L1 holds x is prime Ideal of L2 ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being set st x is prime Ideal of L1 holds x is prime Ideal of L2 let x be set ; ::_thesis: ( x is prime Ideal of L1 implies x is prime Ideal of L2 ) assume x is prime Ideal of L1 ; ::_thesis: x is prime Ideal of L2 then reconsider I = x as prime Ideal of L1 ; reconsider I9 = I as Subset of L2 by A1; reconsider I9 = I9 as Ideal of L2 by A1, WAYBEL_0:3, WAYBEL_0:25; I9 is prime proof let x, y be Element of L2; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I9 or x in I9 or y in I9 ) reconsider a = x, b = y as Element of L1 by A1; A2: x "/\" y = inf {x,y} by YELLOW_0:40; ( ex_inf_of {a,b},L1 & a "/\" b = inf {a,b} ) by YELLOW_0:21, YELLOW_0:40; then a "/\" b = x "/\" y by A1, A2, YELLOW_0:27; hence ( not x "/\" y in I9 or x in I9 or y in I9 ) by Def1; ::_thesis: verum end; hence x is prime Ideal of L2 ; ::_thesis: verum end; definition let L be with_suprema Poset; let F be Filter of L; attrF is prime means :Def2: :: WAYBEL_7:def 2 for x, y being Element of L holds ( not x "\/" y in F or x in F or y in F ); end; :: deftheorem Def2 defines prime WAYBEL_7:def_2_:_ for L being with_suprema Poset for F being Filter of L holds ( F is prime iff for x, y being Element of L holds ( not x "\/" y in F or x in F or y in F ) ); theorem :: WAYBEL_7:14 for L being with_suprema Poset for F being Filter of L holds ( F is prime iff for A being non empty finite Subset of L st sup A in F holds ex a being Element of L st ( a in A & a in F ) ) proof let L be with_suprema Poset; ::_thesis: for F being Filter of L holds ( F is prime iff for A being non empty finite Subset of L st sup A in F holds ex a being Element of L st ( a in A & a in F ) ) let I be Filter of L; ::_thesis: ( I is prime iff for A being non empty finite Subset of L st sup A in I holds ex a being Element of L st ( a in A & a in I ) ) thus ( I is prime implies for A being non empty finite Subset of L st sup A in I holds ex a being Element of L st ( a in A & a in I ) ) ::_thesis: ( ( for A being non empty finite Subset of L st sup A in I holds ex a being Element of L st ( a in A & a in I ) ) implies I is prime ) proof defpred S1[ set ] means ( not $1 is empty & "\/" ($1,L) in I implies ex a being Element of L st ( a in $1 & a in I ) ); assume A1: for x, y being Element of L holds ( not x "\/" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_2 ::_thesis: for A being non empty finite Subset of L st sup A in I holds ex a being Element of L st ( a in A & a in I ) let A be non empty finite Subset of L; ::_thesis: ( sup A in I implies ex a being Element of L st ( a in A & a in I ) ) A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] ) assume that A3: x in A and A4: B c= A and A5: S1[B] ; ::_thesis: S1[B \/ {x}] thus S1[B \/ {x}] ::_thesis: verum proof reconsider a = x as Element of L by A3; reconsider C = B as finite Subset of L by A4, XBOOLE_1:1; assume that not B \/ {x} is empty and A6: "\/" ((B \/ {x}),L) in I ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) then ( "\/" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39; hence ex a being Element of L st ( a in B \/ {x} & a in I ) by A6; ::_thesis: verum end; supposeA7: B <> {} ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) A8: sup {a} = a by YELLOW_0:39; A9: ex_sup_of {a},L by YELLOW_0:54; ex_sup_of C,L by A7, YELLOW_0:54; then A10: "\/" ((B \/ {x}),L) = (sup C) "\/" (sup {a}) by A9, YELLOW_2:3; hereby ::_thesis: verum percases ( sup C in I or a in I ) by A1, A6, A10, A8; suppose sup C in I ; ::_thesis: ex b being Element of L st ( b in B \/ {x} & b in I ) then consider b being Element of L such that A11: ( b in B & b in I ) by A5, A7; take b = b; ::_thesis: ( b in B \/ {x} & b in I ) thus ( b in B \/ {x} & b in I ) by A11, XBOOLE_0:def_3; ::_thesis: verum end; supposeA12: a in I ; ::_thesis: ex a being Element of L st ( a in B \/ {x} & a in I ) take a = a; ::_thesis: ( a in B \/ {x} & a in I ) a in {a} by TARSKI:def_1; hence ( a in B \/ {x} & a in I ) by A12, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; end; end; end; A13: S1[ {} ] ; A14: A is finite ; S1[A] from FINSET_1:sch_2(A14, A13, A2); hence ( sup A in I implies ex a being Element of L st ( a in A & a in I ) ) ; ::_thesis: verum end; assume A15: for A being non empty finite Subset of L st sup A in I holds ex a being Element of L st ( a in A & a in I ) ; ::_thesis: I is prime let a, b be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not a "\/" b in I or a in I or b in I ) assume a "\/" b in I ; ::_thesis: ( a in I or b in I ) then sup {a,b} in I by YELLOW_0:41; then ex x being Element of L st ( x in {a,b} & x in I ) by A15; hence ( a in I or b in I ) by TARSKI:def_2; ::_thesis: verum end; registration let L be LATTICE; cluster non empty filtered upper prime for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is prime proof take [#] L ; ::_thesis: [#] L is prime let x, y be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in [#] L or x in [#] L or y in [#] L ) thus ( not x "\/" y in [#] L or x in [#] L or y in [#] L ) ; ::_thesis: verum end; end; theorem Th15: :: WAYBEL_7:15 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being set st x is prime Filter of L1 holds x is prime Filter of L2 proof let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being set st x is prime Filter of L1 holds x is prime Filter of L2 ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being set st x is prime Filter of L1 holds x is prime Filter of L2 let x be set ; ::_thesis: ( x is prime Filter of L1 implies x is prime Filter of L2 ) assume x is prime Filter of L1 ; ::_thesis: x is prime Filter of L2 then reconsider I = x as prime Filter of L1 ; reconsider I9 = I as Subset of L2 by A1; reconsider I9 = I9 as Filter of L2 by A1, WAYBEL_0:4, WAYBEL_0:25; I9 is prime proof let x, y be Element of L2; :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in I9 or x in I9 or y in I9 ) reconsider a = x, b = y as Element of L1 by A1; A2: x "\/" y = sup {x,y} by YELLOW_0:41; ( ex_sup_of {a,b},L1 & a "\/" b = sup {a,b} ) by YELLOW_0:20, YELLOW_0:41; then a "\/" b = x "\/" y by A1, A2, YELLOW_0:26; hence ( not x "\/" y in I9 or x in I9 or y in I9 ) by Def2; ::_thesis: verum end; hence x is prime Filter of L2 ; ::_thesis: verum end; theorem Th16: :: WAYBEL_7:16 for L being LATTICE for x being set holds ( x is prime Ideal of L iff x is prime Filter of (L opp) ) proof let L be LATTICE; ::_thesis: for x being set holds ( x is prime Ideal of L iff x is prime Filter of (L opp) ) let x be set ; ::_thesis: ( x is prime Ideal of L iff x is prime Filter of (L opp) ) hereby ::_thesis: ( x is prime Filter of (L opp) implies x is prime Ideal of L ) assume x is prime Ideal of L ; ::_thesis: x is prime Filter of (L opp) then reconsider I = x as prime Ideal of L ; reconsider F = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28; F is prime proof let x, y be Element of (L opp); :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in F or x in F or y in F ) A1: x "\/" y = (~ x) "/\" (~ y) by YELLOW_7:22; ( ~ x = x & ~ y = y ) by LATTICE3:def_7; hence ( not x "\/" y in F or x in F or y in F ) by A1, Def1; ::_thesis: verum end; hence x is prime Filter of (L opp) ; ::_thesis: verum end; assume x is prime Filter of (L opp) ; ::_thesis: x is prime Ideal of L then reconsider I = x as prime Filter of (L opp) ; reconsider F = I as Ideal of L by YELLOW_7:26, YELLOW_7:28; F is prime proof let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in F or x in F or y in F ) A2: x "/\" y = (x ~) "\/" (y ~) by YELLOW_7:21; ( x ~ = x & y ~ = y ) by LATTICE3:def_6; hence ( not x "/\" y in F or x in F or y in F ) by A2, Def2; ::_thesis: verum end; hence x is prime Ideal of L ; ::_thesis: verum end; theorem Th17: :: WAYBEL_7:17 for L being LATTICE for x being set holds ( x is prime Filter of L iff x is prime Ideal of (L opp) ) proof let L be LATTICE; ::_thesis: for x being set holds ( x is prime Filter of L iff x is prime Ideal of (L opp) ) let x be set ; ::_thesis: ( x is prime Filter of L iff x is prime Ideal of (L opp) ) (L opp) opp = RelStr(# the carrier of L, the InternalRel of L #) by LATTICE3:8; then ( x is prime Filter of L iff x is prime Filter of ((L opp) opp) ) by Th15; hence ( x is prime Filter of L iff x is prime Ideal of (L opp) ) by Th16; ::_thesis: verum end; theorem :: WAYBEL_7:18 for L being with_infima Poset for I being Ideal of L holds ( I is prime iff ( I ` is Filter of L or I ` = {} ) ) proof let L be with_infima Poset; ::_thesis: for I being Ideal of L holds ( I is prime iff ( I ` is Filter of L or I ` = {} ) ) let I be Ideal of L; ::_thesis: ( I is prime iff ( I ` is Filter of L or I ` = {} ) ) set F = I ` ; thus ( not I is prime or I ` is Filter of L or I ` = {} ) ::_thesis: ( ( I ` is Filter of L or I ` = {} ) implies I is prime ) proof assume A1: for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: ( I ` is Filter of L or I ` = {} ) A2: I ` is filtered proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in I ` or not y in I ` or ex b1 being Element of the carrier of L st ( b1 in I ` & b1 <= x & b1 <= y ) ) assume ( x in I ` & y in I ` ) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in I ` & b1 <= x & b1 <= y ) then ( not x in I & not y in I ) by XBOOLE_0:def_5; then A3: x "/\" y in I ` by A1, SUBSET_1:29; ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23; hence ex b1 being Element of the carrier of L st ( b1 in I ` & b1 <= x & b1 <= y ) by A3; ::_thesis: verum end; I ` is upper proof let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in I ` or not x <= y or y in I ` ) assume that A4: x in I ` and A5: y >= x ; ::_thesis: y in I ` ( y in I implies x in I ) by A5, WAYBEL_0:def_19; hence y in I ` by A4, XBOOLE_0:def_5; ::_thesis: verum end; hence ( I ` is Filter of L or I ` = {} ) by A2; ::_thesis: verum end; assume A6: ( I ` is Filter of L or I ` = {} ) ; ::_thesis: I is prime let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I or x in I or y in I ) assume x "/\" y in I ; ::_thesis: ( x in I or y in I ) then not x "/\" y in I ` by XBOOLE_0:def_5; then ( not x in I ` or not y in I ` ) by A6, WAYBEL_0:41; hence ( x in I or y in I ) by SUBSET_1:29; ::_thesis: verum end; theorem :: WAYBEL_7:19 for L being LATTICE for I being Ideal of L holds ( I is prime iff I in PRIME (InclPoset (Ids L)) ) proof let L be LATTICE; ::_thesis: for I being Ideal of L holds ( I is prime iff I in PRIME (InclPoset (Ids L)) ) let I be Ideal of L; ::_thesis: ( I is prime iff I in PRIME (InclPoset (Ids L)) ) set P = InclPoset (Ids L); A1: InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1; I in Ids L ; then reconsider i = I as Element of (InclPoset (Ids L)) by A1; thus ( I is prime implies I in PRIME (InclPoset (Ids L)) ) ::_thesis: ( I in PRIME (InclPoset (Ids L)) implies I is prime ) proof assume A2: for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: I in PRIME (InclPoset (Ids L)) i is prime proof let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= i or x <= i or y <= i ) y in Ids L by A1; then A3: ex J being Ideal of L st y = J ; x in Ids L by A1; then ex J being Ideal of L st x = J ; then reconsider X = x, Y = y as Ideal of L by A3; assume x "/\" y <= i ; ::_thesis: ( x <= i or y <= i ) then x "/\" y c= I by YELLOW_1:3; then A4: X /\ Y c= I by YELLOW_2:43; assume that A5: not x <= i and A6: not y <= i ; ::_thesis: contradiction not X c= I by A5, YELLOW_1:3; then consider a being set such that A7: a in X and A8: not a in I by TARSKI:def_3; not Y c= I by A6, YELLOW_1:3; then consider b being set such that A9: b in Y and A10: not b in I by TARSKI:def_3; reconsider a = a, b = b as Element of L by A7, A9; a "/\" b <= b by YELLOW_0:23; then A11: a "/\" b in Y by A9, WAYBEL_0:def_19; a "/\" b <= a by YELLOW_0:23; then a "/\" b in X by A7, WAYBEL_0:def_19; then a "/\" b in X /\ Y by A11, XBOOLE_0:def_4; hence contradiction by A2, A4, A8, A10; ::_thesis: verum end; hence I in PRIME (InclPoset (Ids L)) by WAYBEL_6:def_7; ::_thesis: verum end; assume A12: I in PRIME (InclPoset (Ids L)) ; ::_thesis: I is prime let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I or x in I or y in I ) reconsider X = downarrow x, Y = downarrow y as Ideal of L ; ( X in Ids L & Y in Ids L ) ; then reconsider X = X, Y = Y as Element of (InclPoset (Ids L)) by A1; A13: X /\ Y = X "/\" Y by YELLOW_2:43; assume A14: x "/\" y in I ; ::_thesis: ( x in I or y in I ) X "/\" Y c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" Y or a in I ) assume A15: a in X "/\" Y ; ::_thesis: a in I then A16: a in X by A13, XBOOLE_0:def_4; A17: a in Y by A13, A15, XBOOLE_0:def_4; reconsider a = a as Element of L by A16; A18: a <= y by A17, WAYBEL_0:17; a <= x by A16, WAYBEL_0:17; then a <= x "/\" y by A18, YELLOW_0:23; hence a in I by A14, WAYBEL_0:def_19; ::_thesis: verum end; then A19: X "/\" Y <= i by YELLOW_1:3; i is prime by A12, WAYBEL_6:def_7; then ( X <= i or Y <= i ) by A19, WAYBEL_6:def_6; then A20: ( X c= I or Y c= I ) by YELLOW_1:3; y <= y ; then A21: y in Y by WAYBEL_0:17; x <= x ; then x in X by WAYBEL_0:17; hence ( x in I or y in I ) by A21, A20; ::_thesis: verum end; theorem Th20: :: WAYBEL_7:20 for L being Boolean LATTICE for F being Filter of L holds ( F is prime iff for a being Element of L holds ( a in F or 'not' a in F ) ) proof let L be Boolean LATTICE; ::_thesis: for F being Filter of L holds ( F is prime iff for a being Element of L holds ( a in F or 'not' a in F ) ) let F be Filter of L; ::_thesis: ( F is prime iff for a being Element of L holds ( a in F or 'not' a in F ) ) hereby ::_thesis: ( ( for a being Element of L holds ( a in F or 'not' a in F ) ) implies F is prime ) assume A1: F is prime ; ::_thesis: for a being Element of L holds ( a in F or 'not' a in F ) let a be Element of L; ::_thesis: ( a in F or 'not' a in F ) set b = 'not' a; a "\/" ('not' a) = Top L by YELLOW_5:34; then a "\/" ('not' a) in F by WAYBEL_4:22; hence ( a in F or 'not' a in F ) by A1, Def2; ::_thesis: verum end; assume A2: for a being Element of L holds ( a in F or 'not' a in F ) ; ::_thesis: F is prime let a, b be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not a "\/" b in F or a in F or b in F ) assume that A3: a "\/" b in F and A4: not a in F and A5: not b in F ; ::_thesis: contradiction ( 'not' a in F & 'not' b in F ) by A2, A4, A5; then ('not' a) "/\" ('not' b) in F by WAYBEL_0:41; then 'not' (a "\/" b) in F by YELLOW_5:36; then ('not' (a "\/" b)) "/\" (a "\/" b) in F by A3, WAYBEL_0:41; then A6: Bottom L in F by YELLOW_5:34; a >= Bottom L by YELLOW_0:44; hence contradiction by A4, A6, WAYBEL_0:def_20; ::_thesis: verum end; theorem Th21: :: WAYBEL_7:21 for X being set for F being Filter of (BoolePoset X) holds ( F is prime iff for A being Subset of X holds ( A in F or X \ A in F ) ) proof let X be set ; ::_thesis: for F being Filter of (BoolePoset X) holds ( F is prime iff for A being Subset of X holds ( A in F or X \ A in F ) ) set L = BoolePoset X; let F be Filter of (BoolePoset X); ::_thesis: ( F is prime iff for A being Subset of X holds ( A in F or X \ A in F ) ) BoolePoset X = InclPoset (bool X) by YELLOW_1:4; then A1: BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1; hereby ::_thesis: ( ( for A being Subset of X holds ( A in F or X \ A in F ) ) implies F is prime ) assume A2: F is prime ; ::_thesis: for A being Subset of X holds ( A in F or X \ A in F ) let A be Subset of X; ::_thesis: ( A in F or X \ A in F ) reconsider a = A as Element of (BoolePoset X) by A1; ( a in F or 'not' a in F ) by A2, Th20; hence ( A in F or X \ A in F ) by Th5; ::_thesis: verum end; assume A3: for A being Subset of X holds ( A in F or X \ A in F ) ; ::_thesis: F is prime now__::_thesis:_for_a_being_Element_of_(BoolePoset_X)_holds_ (_a_in_F_or_'not'_a_in_F_) let a be Element of (BoolePoset X); ::_thesis: ( a in F or 'not' a in F ) 'not' a = X \ a by Th5; hence ( a in F or 'not' a in F ) by A1, A3; ::_thesis: verum end; hence F is prime by Th20; ::_thesis: verum end; definition let L be non empty Poset; let F be Filter of L; attrF is ultra means :Def3: :: WAYBEL_7:def 3 ( F is proper & ( for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) ) ); end; :: deftheorem Def3 defines ultra WAYBEL_7:def_3_:_ for L being non empty Poset for F being Filter of L holds ( F is ultra iff ( F is proper & ( for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) ) ) ); registration let L be non empty Poset; cluster non empty filtered upper ultra -> proper for Element of bool the carrier of L; coherence for b1 being Filter of L st b1 is ultra holds b1 is proper by Def3; end; Lm1: for L being with_infima Poset for F being Filter of L for X being non empty finite Subset of L for x being Element of L st x in uparrow (fininfs (F \/ X)) holds ex a being Element of L st ( a in F & x >= a "/\" (inf X) ) proof let L be with_infima Poset; ::_thesis: for F being Filter of L for X being non empty finite Subset of L for x being Element of L st x in uparrow (fininfs (F \/ X)) holds ex a being Element of L st ( a in F & x >= a "/\" (inf X) ) let I be Filter of L; ::_thesis: for X being non empty finite Subset of L for x being Element of L st x in uparrow (fininfs (I \/ X)) holds ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) let X be non empty finite Subset of L; ::_thesis: for x being Element of L st x in uparrow (fininfs (I \/ X)) holds ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) let x be Element of L; ::_thesis: ( x in uparrow (fininfs (I \/ X)) implies ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) ) set i = the Element of I; reconsider i = the Element of I as Element of L ; assume x in uparrow (fininfs (I \/ X)) ; ::_thesis: ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) then consider u being Element of L such that A1: u <= x and A2: u in fininfs (I \/ X) by WAYBEL_0:def_16; consider Y being finite Subset of (I \/ X) such that A3: u = "/\" (Y,L) and A4: ex_inf_of Y,L by A2; Y \ X c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y \ X or a in I ) assume A5: a in Y \ X ; ::_thesis: a in I then not a in X by XBOOLE_0:def_5; hence a in I by A5, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider Z = Y \ X as finite Subset of I ; reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1; reconsider ZX = Z9 \/ X as finite Subset of L ; percases ( Z = {} or Z <> {} ) ; supposeA6: Z = {} ; ::_thesis: ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) A7: inf X >= i "/\" (inf X) by YELLOW_0:23; take i ; ::_thesis: ( i in I & x >= i "/\" (inf X) ) A8: ex_inf_of X,L by YELLOW_0:55; Y c= X by A6, XBOOLE_1:37; then u >= inf X by A3, A4, A8, YELLOW_0:35; then u >= i "/\" (inf X) by A7, ORDERS_2:3; hence ( i in I & x >= i "/\" (inf X) ) by A1, ORDERS_2:3; ::_thesis: verum end; supposeA9: Z <> {} ; ::_thesis: ex a being Element of L st ( a in I & x >= a "/\" (inf X) ) take inf Z9 ; ::_thesis: ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) ) A10: ex_inf_of X,L by YELLOW_0:55; A11: ex_inf_of ZX,L by YELLOW_0:55; Y c= Y \/ X by XBOOLE_1:7; then Y c= Z9 \/ X by XBOOLE_1:39; then A12: inf Y9 >= inf ZX by A4, A11, YELLOW_0:35; ex_inf_of Z9,L by A9, YELLOW_0:55; then inf (Z9 \/ X) = (inf Z9) "/\" (inf X) by A10, A11, YELLOW_0:37; hence ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:43; ::_thesis: verum end; end; end; theorem Th22: :: WAYBEL_7:22 for L being Boolean LATTICE for F being Filter of L holds ( ( F is proper & F is prime ) iff F is ultra ) proof let L be Boolean LATTICE; ::_thesis: for F being Filter of L holds ( ( F is proper & F is prime ) iff F is ultra ) let F be Filter of L; ::_thesis: ( ( F is proper & F is prime ) iff F is ultra ) thus ( F is proper & F is prime implies F is ultra ) ::_thesis: ( F is ultra implies ( F is proper & F is prime ) ) proof assume A1: F is proper ; ::_thesis: ( not F is prime or F is ultra ) assume A2: for x, y being Element of L holds ( not x "\/" y in F or x in F or y in F ) ; :: according to WAYBEL_7:def_2 ::_thesis: F is ultra thus F is proper by A1; :: according to WAYBEL_7:def_3 ::_thesis: for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) let G be Filter of L; ::_thesis: ( not F c= G or F = G or G = the carrier of L ) assume that A3: F c= G and A4: F <> G ; ::_thesis: G = the carrier of L consider x being set such that A5: ( ( x in F & not x in G ) or ( x in G & not x in F ) ) by A4, TARSKI:1; reconsider x = x as Element of L by A5; set y = 'not' x; x "\/" ('not' x) = Top L by YELLOW_5:34; then 'not' x in F by A2, A3, A5, WAYBEL_4:22; then x "/\" ('not' x) in G by A3, A5, WAYBEL_0:41; then A6: Bottom L in G by YELLOW_5:34; thus G c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= G let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in G ) assume x in the carrier of L ; ::_thesis: x in G then reconsider x = x as Element of L ; x >= Bottom L by YELLOW_0:44; hence x in G by A6, WAYBEL_0:def_20; ::_thesis: verum end; assume that A7: F is proper and A8: for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) ; :: according to WAYBEL_7:def_3 ::_thesis: ( F is proper & F is prime ) thus F is proper by A7; ::_thesis: F is prime now__::_thesis:_for_a_being_Element_of_L_st_not_a_in_F_holds_ 'not'_a_in_F let a be Element of L; ::_thesis: ( not a in F implies 'not' a in F ) assume that A9: not a in F and A10: not 'not' a in F ; ::_thesis: contradiction set b = 'not' a; A11: F \/ {a} c= uparrow (fininfs (F \/ {a})) by WAYBEL_0:62; ( {a} c= F \/ {a} & a in {a} ) by TARSKI:def_1, XBOOLE_1:7; then a in F \/ {a} ; then ( F c= F \/ {a} & a in uparrow (fininfs (F \/ {a})) ) by A11, XBOOLE_1:7; then uparrow (fininfs (F \/ {a})) = the carrier of L by A8, A9, A11, XBOOLE_1:1; then consider c being Element of L such that A12: c in F and A13: 'not' a >= c "/\" (inf {a}) by Lm1; c <= Top L by YELLOW_0:45; then A14: c = c "/\" (Top L) by YELLOW_0:25 .= c "/\" (a "\/" ('not' a)) by YELLOW_5:34 .= (c "/\" a) "\/" (c "/\" ('not' a)) by WAYBEL_1:def_3 ; ( inf {a} = a & c "/\" ('not' a) <= 'not' a ) by YELLOW_0:23, YELLOW_0:39; then c <= 'not' a by A13, A14, YELLOW_0:22; hence contradiction by A10, A12, WAYBEL_0:def_20; ::_thesis: verum end; hence F is prime by Th20; ::_thesis: verum end; Lm2: for L being with_suprema Poset for I being Ideal of L for X being non empty finite Subset of L for x being Element of L st x in downarrow (finsups (I \/ X)) holds ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) proof let L be with_suprema Poset; ::_thesis: for I being Ideal of L for X being non empty finite Subset of L for x being Element of L st x in downarrow (finsups (I \/ X)) holds ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) let I be Ideal of L; ::_thesis: for X being non empty finite Subset of L for x being Element of L st x in downarrow (finsups (I \/ X)) holds ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) let X be non empty finite Subset of L; ::_thesis: for x being Element of L st x in downarrow (finsups (I \/ X)) holds ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) let x be Element of L; ::_thesis: ( x in downarrow (finsups (I \/ X)) implies ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) ) set i = the Element of I; reconsider i = the Element of I as Element of L ; assume x in downarrow (finsups (I \/ X)) ; ::_thesis: ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) then consider u being Element of L such that A1: u >= x and A2: u in finsups (I \/ X) by WAYBEL_0:def_15; consider Y being finite Subset of (I \/ X) such that A3: u = "\/" (Y,L) and A4: ex_sup_of Y,L by A2; Y \ X c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y \ X or a in I ) assume A5: a in Y \ X ; ::_thesis: a in I then not a in X by XBOOLE_0:def_5; hence a in I by A5, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider Z = Y \ X as finite Subset of I ; reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1; reconsider ZX = Z9 \/ X as finite Subset of L ; percases ( Z = {} or Z <> {} ) ; supposeA6: Z = {} ; ::_thesis: ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) A7: sup X <= i "\/" (sup X) by YELLOW_0:22; take i ; ::_thesis: ( i in I & x <= i "\/" (sup X) ) A8: ex_sup_of X,L by YELLOW_0:54; Y c= X by A6, XBOOLE_1:37; then u <= sup X by A3, A4, A8, YELLOW_0:34; then u <= i "\/" (sup X) by A7, ORDERS_2:3; hence ( i in I & x <= i "\/" (sup X) ) by A1, ORDERS_2:3; ::_thesis: verum end; supposeA9: Z <> {} ; ::_thesis: ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) take sup Z9 ; ::_thesis: ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) ) A10: ex_sup_of X,L by YELLOW_0:54; A11: ex_sup_of ZX,L by YELLOW_0:54; Y c= Y \/ X by XBOOLE_1:7; then Y c= Z9 \/ X by XBOOLE_1:39; then A12: sup Y9 <= sup ZX by A4, A11, YELLOW_0:34; ex_sup_of Z9,L by A9, YELLOW_0:54; then sup (Z9 \/ X) = (sup Z9) "\/" (sup X) by A10, A11, YELLOW_0:36; hence ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:42; ::_thesis: verum end; end; end; theorem Th23: :: WAYBEL_7:23 for L being distributive LATTICE for I being Ideal of L for F being Filter of L st I misses F holds ex P being Ideal of L st ( P is prime & I c= P & P misses F ) proof let L be distributive LATTICE; ::_thesis: for I being Ideal of L for F being Filter of L st I misses F holds ex P being Ideal of L st ( P is prime & I c= P & P misses F ) let I be Ideal of L; ::_thesis: for F being Filter of L st I misses F holds ex P being Ideal of L st ( P is prime & I c= P & P misses F ) let F be Filter of L; ::_thesis: ( I misses F implies ex P being Ideal of L st ( P is prime & I c= P & P misses F ) ) assume A1: I misses F ; ::_thesis: ex P being Ideal of L st ( P is prime & I c= P & P misses F ) set X = { P where P is Ideal of L : ( I c= P & P misses F ) } ; A2: now__::_thesis:_for_A_being_set_st_A_in__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}__holds_ (_I_c=_A_&_A_misses_F_) let A be set ; ::_thesis: ( A in { P where P is Ideal of L : ( I c= P & P misses F ) } implies ( I c= A & A misses F ) ) assume A in { P where P is Ideal of L : ( I c= P & P misses F ) } ; ::_thesis: ( I c= A & A misses F ) then ex P being Ideal of L st ( A = P & I c= P & P misses F ) ; hence ( I c= A & A misses F ) ; ::_thesis: verum end; A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}__&_Z_is_c=-linear_holds_ union_Z_in__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}_ let Z be set ; ::_thesis: ( Z <> {} & Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } & Z is c=-linear implies union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } ) assume that A4: Z <> {} and A5: Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } and A6: Z is c=-linear ; ::_thesis: union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } Z c= bool the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in bool the carrier of L ) assume x in Z ; ::_thesis: x in bool the carrier of L then x in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5; then ex P being Ideal of L st ( x = P & I c= P & P misses F ) ; hence x in bool the carrier of L ; ::_thesis: verum end; then reconsider ZI = Z as Subset-Family of L ; now__::_thesis:_for_A_being_Subset_of_L_st_A_in_ZI_holds_ A_is_lower let A be Subset of L; ::_thesis: ( A in ZI implies A is lower ) assume A in ZI ; ::_thesis: A is lower then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5; then ex P being Ideal of L st ( A = P & I c= P & P misses F ) ; hence A is lower ; ::_thesis: verum end; then reconsider J = union ZI as lower Subset of L by WAYBEL_0:26; A7: now__::_thesis:_(_I_c=_J_&_not_J_is_empty_&_(_for_A,_B_being_Subset_of_L_st_A_in_ZI_&_B_in_ZI_holds_ ex_C_being_Subset_of_L_st_ (_C_in_ZI_&_A_\/_B_c=_C_)_)_) set y = the Element of Z; the Element of Z in Z by A4; then A8: I c= the Element of Z by A2, A5; A9: the Element of Z c= J by A4, ZFMISC_1:74; hence I c= J by A8, XBOOLE_1:1; ::_thesis: ( not J is empty & ( for A, B being Subset of L st A in ZI & B in ZI holds ex C being Subset of L st ( C in ZI & A \/ B c= C ) ) ) thus not J is empty by A8, A9; ::_thesis: for A, B being Subset of L st A in ZI & B in ZI holds ex C being Subset of L st ( C in ZI & A \/ B c= C ) let A, B be Subset of L; ::_thesis: ( A in ZI & B in ZI implies ex C being Subset of L st ( C in ZI & A \/ B c= C ) ) assume A10: ( A in ZI & B in ZI ) ; ::_thesis: ex C being Subset of L st ( C in ZI & A \/ B c= C ) then A,B are_c=-comparable by A6, ORDINAL1:def_8; then ( A c= B or B c= A ) by XBOOLE_0:def_9; then ( A \/ B = A or A \/ B = B ) by XBOOLE_1:12; hence ex C being Subset of L st ( C in ZI & A \/ B c= C ) by A10; ::_thesis: verum end; now__::_thesis:_for_A_being_Subset_of_L_st_A_in_ZI_holds_ A_is_directed let A be Subset of L; ::_thesis: ( A in ZI implies A is directed ) assume A in ZI ; ::_thesis: A is directed then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5; then ex P being Ideal of L st ( A = P & I c= P & P misses F ) ; hence A is directed ; ::_thesis: verum end; then reconsider J = J as Ideal of L by A7, WAYBEL_0:46; now__::_thesis:_for_x_being_set_st_x_in_J_holds_ not_x_in_F let x be set ; ::_thesis: ( x in J implies not x in F ) assume x in J ; ::_thesis: not x in F then consider A being set such that A11: x in A and A12: A in Z by TARSKI:def_4; A misses F by A2, A5, A12; hence not x in F by A11, XBOOLE_0:3; ::_thesis: verum end; then J misses F by XBOOLE_0:3; hence union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } by A7; ::_thesis: verum end; I in { P where P is Ideal of L : ( I c= P & P misses F ) } by A1; then consider Y being set such that A13: Y in { P where P is Ideal of L : ( I c= P & P misses F ) } and A14: for Z being set st Z in { P where P is Ideal of L : ( I c= P & P misses F ) } & Z <> Y holds not Y c= Z by A3, ORDERS_1:67; consider P being Ideal of L such that A15: P = Y and A16: I c= P and A17: P misses F by A13; take P ; ::_thesis: ( P is prime & I c= P & P misses F ) hereby :: according to WAYBEL_7:def_1 ::_thesis: ( I c= P & P misses F ) let x, y be Element of L; ::_thesis: ( x "/\" y in P & not x in P implies y in P ) assume that A18: x "/\" y in P and A19: not x in P and A20: not y in P ; ::_thesis: contradiction set Py = downarrow (finsups (P \/ {y})); A21: P \/ {y} c= downarrow (finsups (P \/ {y})) by WAYBEL_0:61; A22: P c= P \/ {y} by XBOOLE_1:7; then P c= downarrow (finsups (P \/ {y})) by A21, XBOOLE_1:1; then A23: I c= downarrow (finsups (P \/ {y})) by A16, XBOOLE_1:1; y in {y} by TARSKI:def_1; then y in P \/ {y} by XBOOLE_0:def_3; then A24: y in downarrow (finsups (P \/ {y})) by A21; now__::_thesis:_not_downarrow_(finsups_(P_\/_{y}))_misses_F assume downarrow (finsups (P \/ {y})) misses F ; ::_thesis: contradiction then downarrow (finsups (P \/ {y})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A23; hence contradiction by A14, A15, A20, A21, A22, A24, XBOOLE_1:1; ::_thesis: verum end; then consider v being set such that A25: v in downarrow (finsups (P \/ {y})) and A26: v in F by XBOOLE_0:3; set Px = downarrow (finsups (P \/ {x})); A27: P \/ {x} c= downarrow (finsups (P \/ {x})) by WAYBEL_0:61; A28: P c= P \/ {x} by XBOOLE_1:7; then P c= downarrow (finsups (P \/ {x})) by A27, XBOOLE_1:1; then A29: I c= downarrow (finsups (P \/ {x})) by A16, XBOOLE_1:1; x in {x} by TARSKI:def_1; then x in P \/ {x} by XBOOLE_0:def_3; then A30: x in downarrow (finsups (P \/ {x})) by A27; now__::_thesis:_not_downarrow_(finsups_(P_\/_{x}))_misses_F assume downarrow (finsups (P \/ {x})) misses F ; ::_thesis: contradiction then downarrow (finsups (P \/ {x})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A29; hence contradiction by A14, A15, A19, A27, A28, A30, XBOOLE_1:1; ::_thesis: verum end; then consider u being set such that A31: u in downarrow (finsups (P \/ {x})) and A32: u in F by XBOOLE_0:3; reconsider u = u, v = v as Element of L by A31, A25; consider u9 being Element of L such that A33: u9 in P and A34: u <= u9 "\/" (sup {x}) by A31, Lm2; consider v9 being Element of L such that A35: v9 in P and A36: v <= v9 "\/" (sup {y}) by A25, Lm2; set w = u9 "\/" v9; (v9 "\/" u9) "\/" x = v9 "\/" (u9 "\/" x) by LATTICE3:14; then ( sup {x} = x & (u9 "\/" v9) "\/" x >= u9 "\/" x ) by YELLOW_0:22, YELLOW_0:39; then (u9 "\/" v9) "\/" x >= u by A34, ORDERS_2:3; then A37: (u9 "\/" v9) "\/" x in F by A32, WAYBEL_0:def_20; (u9 "\/" v9) "\/" y = u9 "\/" (v9 "\/" y) by LATTICE3:14; then ( sup {y} = y & (u9 "\/" v9) "\/" y >= v9 "\/" y ) by YELLOW_0:22, YELLOW_0:39; then (u9 "\/" v9) "\/" y >= v by A36, ORDERS_2:3; then (u9 "\/" v9) "\/" y in F by A26, WAYBEL_0:def_20; then ((u9 "\/" v9) "\/" x) "/\" ((u9 "\/" v9) "\/" y) in F by A37, WAYBEL_0:41; then A38: (u9 "\/" v9) "\/" (x "/\" y) in F by WAYBEL_1:5; u9 "\/" v9 in P by A33, A35, WAYBEL_0:40; then (u9 "\/" v9) "\/" (x "/\" y) in P by A18, WAYBEL_0:40; hence contradiction by A17, A38, XBOOLE_0:3; ::_thesis: verum end; thus ( I c= P & P misses F ) by A16, A17; ::_thesis: verum end; theorem Th24: :: WAYBEL_7:24 for L being distributive LATTICE for I being Ideal of L for x being Element of L st not x in I holds ex P being Ideal of L st ( P is prime & I c= P & not x in P ) proof let L be distributive LATTICE; ::_thesis: for I being Ideal of L for x being Element of L st not x in I holds ex P being Ideal of L st ( P is prime & I c= P & not x in P ) let I be Ideal of L; ::_thesis: for x being Element of L st not x in I holds ex P being Ideal of L st ( P is prime & I c= P & not x in P ) let x be Element of L; ::_thesis: ( not x in I implies ex P being Ideal of L st ( P is prime & I c= P & not x in P ) ) assume A1: not x in I ; ::_thesis: ex P being Ideal of L st ( P is prime & I c= P & not x in P ) now__::_thesis:_for_a_being_set_st_a_in_I_holds_ not_a_in_uparrow_x let a be set ; ::_thesis: ( a in I implies not a in uparrow x ) assume that A2: a in I and A3: a in uparrow x ; ::_thesis: contradiction reconsider a = a as Element of L by A2; a >= x by A3, WAYBEL_0:18; hence contradiction by A1, A2, WAYBEL_0:def_19; ::_thesis: verum end; then I misses uparrow x by XBOOLE_0:3; then consider P being Ideal of L such that A4: ( P is prime & I c= P ) and A5: P misses uparrow x by Th23; take P ; ::_thesis: ( P is prime & I c= P & not x in P ) thus ( P is prime & I c= P ) by A4; ::_thesis: not x in P assume x in P ; ::_thesis: contradiction then not x in uparrow x by A5, XBOOLE_0:3; then not x <= x by WAYBEL_0:18; hence contradiction ; ::_thesis: verum end; theorem Th25: :: WAYBEL_7:25 for L being distributive LATTICE for I being Ideal of L for F being Filter of L st I misses F holds ex P being Filter of L st ( P is prime & F c= P & I misses P ) proof let L be distributive LATTICE; ::_thesis: for I being Ideal of L for F being Filter of L st I misses F holds ex P being Filter of L st ( P is prime & F c= P & I misses P ) let I be Ideal of L; ::_thesis: for F being Filter of L st I misses F holds ex P being Filter of L st ( P is prime & F c= P & I misses P ) let F be Filter of L; ::_thesis: ( I misses F implies ex P being Filter of L st ( P is prime & F c= P & I misses P ) ) assume A1: I misses F ; ::_thesis: ex P being Filter of L st ( P is prime & F c= P & I misses P ) reconsider I9 = F as Ideal of (L opp) by YELLOW_7:27, YELLOW_7:29; reconsider F9 = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28; consider P9 being Ideal of (L opp) such that A2: ( P9 is prime & I9 c= P9 & P9 misses F9 ) by A1, Th23; reconsider P = P9 as Filter of L by YELLOW_7:27, YELLOW_7:29; take P ; ::_thesis: ( P is prime & F c= P & I misses P ) thus ( P is prime & F c= P & I misses P ) by A2, Th17; ::_thesis: verum end; theorem Th26: :: WAYBEL_7:26 for L being non trivial Boolean LATTICE for F being proper Filter of L ex G being Filter of L st ( F c= G & G is ultra ) proof let L be non trivial Boolean LATTICE; ::_thesis: for F being proper Filter of L ex G being Filter of L st ( F c= G & G is ultra ) let F be proper Filter of L; ::_thesis: ex G being Filter of L st ( F c= G & G is ultra ) downarrow (Bottom L) = {(Bottom L)} by WAYBEL_4:23; then reconsider I = {(Bottom L)} as Ideal of L ; now__::_thesis:_for_a_being_set_st_a_in_I_holds_ not_a_in_F let a be set ; ::_thesis: ( a in I implies not a in F ) assume a in I ; ::_thesis: not a in F then a = Bottom L by TARSKI:def_1; hence not a in F by Th4; ::_thesis: verum end; then I misses F by XBOOLE_0:3; then consider G being Filter of L such that A1: ( G is prime & F c= G ) and A2: I misses G by Th25; take G ; ::_thesis: ( F c= G & G is ultra ) now__::_thesis:_not_Bottom_L_in_G assume Bottom L in G ; ::_thesis: contradiction then not Bottom L in I by A2, XBOOLE_0:3; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then G is proper by Th4; hence ( F c= G & G is ultra ) by A1, Th22; ::_thesis: verum end; begin definition let T be TopSpace; let F, x be set ; predx is_a_cluster_point_of F,T means :Def4: :: WAYBEL_7:def 4 for A being Subset of T st A is open & x in A holds for B being set st B in F holds A meets B; predx is_a_convergence_point_of F,T means :Def5: :: WAYBEL_7:def 5 for A being Subset of T st A is open & x in A holds A in F; end; :: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def_4_:_ for T being TopSpace for F, x being set holds ( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds for B being set st B in F holds A meets B ); :: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def_5_:_ for T being TopSpace for F, x being set holds ( x is_a_convergence_point_of F,T iff for A being Subset of T st A is open & x in A holds A in F ); registration let X be non empty set ; cluster non empty filtered upper ultra for Element of bool the carrier of (BoolePoset X); existence ex b1 being Filter of (BoolePoset X) st b1 is ultra proof set F = the proper Filter of (BoolePoset X); ex G being Filter of (BoolePoset X) st ( the proper Filter of (BoolePoset X) c= G & G is ultra ) by Th26; hence ex b1 being Filter of (BoolePoset X) st b1 is ultra ; ::_thesis: verum end; end; theorem Th27: :: WAYBEL_7:27 for T being non empty TopSpace for F being ultra Filter of (BoolePoset the carrier of T) for p being set holds ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: for F being ultra Filter of (BoolePoset the carrier of T) for p being set holds ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T ) set L = BoolePoset the carrier of T; let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: for p being set holds ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T ) let p be set ; ::_thesis: ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T ) thus ( p is_a_cluster_point_of F,T implies p is_a_convergence_point_of F,T ) ::_thesis: ( p is_a_convergence_point_of F,T implies p is_a_cluster_point_of F,T ) proof assume A1: for A being Subset of T st A is open & p in A holds for B being set st B in F holds A meets B ; :: according to WAYBEL_7:def_4 ::_thesis: p is_a_convergence_point_of F,T let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( A is open & p in A implies A in F ) assume that A2: ( A is open & p in A ) and A3: not A in F ; ::_thesis: contradiction F is prime by Th22; then the carrier of T \ A in F by A3, Th21; then A meets the carrier of T \ A by A1, A2; hence contradiction by XBOOLE_1:79; ::_thesis: verum end; assume A4: for A being Subset of T st A is open & p in A holds A in F ; :: according to WAYBEL_7:def_5 ::_thesis: p is_a_cluster_point_of F,T let A be Subset of T; :: according to WAYBEL_7:def_4 ::_thesis: ( A is open & p in A implies for B being set st B in F holds A meets B ) assume ( A is open & p in A ) ; ::_thesis: for B being set st B in F holds A meets B then A5: A in F by A4; Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18; then A6: not {} in F by Th4; let B be set ; ::_thesis: ( B in F implies A meets B ) assume A7: B in F ; ::_thesis: A meets B then reconsider a = A, b = B as Element of (BoolePoset the carrier of T) by A5; a "/\" b = A /\ B by YELLOW_1:17; then A /\ B in F by A5, A7, WAYBEL_0:41; hence A meets B by A6, XBOOLE_0:def_7; ::_thesis: verum end; theorem Th28: :: WAYBEL_7:28 for T being non empty TopSpace for x, y being Element of (InclPoset the topology of T) st x << y holds for F being proper Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) proof defpred S1[ set , set ] means $1 misses $2; let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds for F being proper Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) set L = InclPoset the topology of T; set B = BoolePoset the carrier of T; let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies for F being proper Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) ) assume A1: x << y ; ::_thesis: for F being proper Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4; then A2: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1; ( x in the carrier of (InclPoset the topology of T) & InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) ) by YELLOW_1:def_1; then reconsider x9 = x as Element of (BoolePoset the carrier of T) by A2; let F be proper Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) ) assume that A3: x in F and A4: for x being Element of T st x in y holds not x is_a_cluster_point_of F,T ; ::_thesis: contradiction set V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st ( B in F & A misses B ) ) } ; { A where A is Subset of T : ( A is open & A meets y & ex B being set st ( B in F & A misses B ) ) } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st ( B in F & A misses B ) ) } or a in bool the carrier of T ) assume a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st ( B in F & A misses B ) ) } ; ::_thesis: a in bool the carrier of T then ex C being Subset of T st ( a = C & C is open & C meets y & ex B being set st ( B in F & C misses B ) ) ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st ( B in F & A misses B ) ) } as Subset-Family of T ; reconsider V = V as Subset-Family of T ; A5: y c= union V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in y or x in union V ) assume A6: x in y ; ::_thesis: x in union V InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1; then y in the topology of T ; then not x is_a_cluster_point_of F,T by A4, A6; then consider A being Subset of T such that A7: A is open and A8: x in A and A9: ex B being set st ( B in F & A misses B ) by Def4; A meets y by A6, A8, XBOOLE_0:3; then A in V by A7, A9; hence x in union V by A8, TARSKI:def_4; ::_thesis: verum end; V is open proof let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in V or a is open ) assume a in V ; ::_thesis: a is open then ex C being Subset of T st ( a = C & C is open & C meets y & ex B being set st ( B in F & C misses B ) ) ; hence a is open ; ::_thesis: verum end; then consider W being finite Subset of V such that A10: x c= union W by A1, A5, WAYBEL_3:34; A11: now__::_thesis:_for_A_being_set_st_A_in_W_holds_ ex_B_being_set_st_ (_B_in_F_&_S1[A,B]_) let A be set ; ::_thesis: ( A in W implies ex B being set st ( B in F & S1[A,B] ) ) assume A in W ; ::_thesis: ex B being set st ( B in F & S1[A,B] ) then A in V ; then ex C being Subset of T st ( A = C & C is open & C meets y & ex B being set st ( B in F & C misses B ) ) ; hence ex B being set st ( B in F & S1[A,B] ) ; ::_thesis: verum end; consider f being Function such that A12: ( dom f = W & rng f c= F & ( for A being set st A in W holds S1[A,f . A] ) ) from FUNCT_1:sch_5(A11); rng f is finite by A12, FINSET_1:8; then consider z being Element of (BoolePoset the carrier of T) such that A13: z in F and A14: z is_<=_than rng f by A12, WAYBEL_0:2; set a = the Element of x9 "/\" z; x9 "/\" z in F by A3, A13, WAYBEL_0:41; then x9 "/\" z <> Bottom (BoolePoset the carrier of T) by Th4; then x9 "/\" z <> {} by YELLOW_1:18; then A15: the Element of x9 "/\" z in x9 "/\" z ; A16: x9 "/\" z c= x9 /\ z by YELLOW_1:17; then the Element of x9 "/\" z in x by A15, XBOOLE_0:def_4; then consider A being set such that A17: the Element of x9 "/\" z in A and A18: A in W by A10, TARSKI:def_4; A19: the Element of x9 "/\" z in z by A15, A16, XBOOLE_0:def_4; A20: f . A in rng f by A12, A18, FUNCT_1:def_3; then f . A in F by A12; then reconsider b = f . A as Element of (BoolePoset the carrier of T) ; z <= b by A14, A20, LATTICE3:def_8; then A21: z c= b by YELLOW_1:2; A misses b by A12, A18; hence contradiction by A19, A17, A21, XBOOLE_0:3; ::_thesis: verum end; theorem :: WAYBEL_7:29 for T being non empty TopSpace for x, y being Element of (InclPoset the topology of T) st x << y holds for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) assume A1: x << y ; ::_thesis: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) assume x in F ; ::_thesis: ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) then consider p being Element of T such that A2: ( p in y & p is_a_cluster_point_of F,T ) by A1, Th28; take p ; ::_thesis: ( p in y & p is_a_convergence_point_of F,T ) thus ( p in y & p is_a_convergence_point_of F,T ) by A2, Th27; ::_thesis: verum end; theorem Th30: :: WAYBEL_7:30 for T being non empty TopSpace for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) holds x << y proof let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) holds x << y set B = BoolePoset the carrier of T; let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) implies x << y ) assume that A1: x c= y and A2: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ; ::_thesis: x << y InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1; then x in the topology of T ; then reconsider X = x as Subset of T ; reconsider X = X as Subset of T ; assume not x << y ; ::_thesis: contradiction then consider F being Subset-Family of T such that A3: F is open and A4: y c= union F and A5: for G being finite Subset of F holds not x c= union G by WAYBEL_3:35; set xF = { (x \ z) where z is Subset of T : z in F } ; set z = the Element of F; A6: now__::_thesis:_not_F_=_{} assume A7: F = {} ; ::_thesis: contradiction then A8: y = {} by A4, ZFMISC_1:2; then x = y by A1; hence contradiction by A1, A4, A5, A7, A8; ::_thesis: verum end; then A9: the Element of F in F ; BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4; then A10: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1; { (x \ z) where z is Subset of T : z in F } c= the carrier of (BoolePoset the carrier of T) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x \ z) where z is Subset of T : z in F } or a in the carrier of (BoolePoset the carrier of T) ) assume a in { (x \ z) where z is Subset of T : z in F } ; ::_thesis: a in the carrier of (BoolePoset the carrier of T) then ex z being Subset of T st ( a = x \ z & z in F ) ; then a c= X ; then a c= the carrier of T by XBOOLE_1:1; hence a in the carrier of (BoolePoset the carrier of T) by A10; ::_thesis: verum end; then reconsider xF = { (x \ z) where z is Subset of T : z in F } as Subset of (BoolePoset the carrier of T) ; set FF = uparrow (fininfs xF); now__::_thesis:_not_Bottom_(BoolePoset_the_carrier_of_T)_in_uparrow_(fininfs_xF) defpred S1[ set , set ] means $1 = x \ $2; assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs xF) ; ::_thesis: contradiction then consider a being Element of (BoolePoset the carrier of T) such that A11: a <= Bottom (BoolePoset the carrier of T) and A12: a in fininfs xF by WAYBEL_0:def_16; consider s being finite Subset of xF such that A13: a = "/\" (s,(BoolePoset the carrier of T)) and ex_inf_of s, BoolePoset the carrier of T by A12; reconsider t = s as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1; A14: now__::_thesis:_for_v_being_set_st_v_in_s_holds_ ex_z_being_set_st_ (_z_in_F_&_S1[v,z]_) let v be set ; ::_thesis: ( v in s implies ex z being set st ( z in F & S1[v,z] ) ) assume v in s ; ::_thesis: ex z being set st ( z in F & S1[v,z] ) then v in xF ; then ex z being Subset of T st ( v = x \ z & z in F ) ; hence ex z being set st ( z in F & S1[v,z] ) ; ::_thesis: verum end; consider f being Function such that A15: ( dom f = s & rng f c= F & ( for v being set st v in s holds S1[v,f . v] ) ) from FUNCT_1:sch_5(A14); reconsider G = rng f as finite Subset of F by A15, FINSET_1:8; Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18; then A16: a c= {} by A11, YELLOW_1:2; A17: now__::_thesis:_not_s_=_{} assume s = {} ; ::_thesis: contradiction then a = Top (BoolePoset the carrier of T) by A13; hence contradiction by A16, YELLOW_1:19; ::_thesis: verum end; then A18: a = meet t by A13, YELLOW_1:20; x c= union G proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in x or c in union G ) assume that A19: c in x and A20: not c in union G ; ::_thesis: contradiction now__::_thesis:_for_v_being_set_st_v_in_s_holds_ c_in_v let v be set ; ::_thesis: ( v in s implies c in v ) assume A21: v in s ; ::_thesis: c in v then f . v in rng f by A15, FUNCT_1:def_3; then A22: not c in f . v by A20, TARSKI:def_4; v = x \ (f . v) by A15, A21; hence c in v by A19, A22, XBOOLE_0:def_5; ::_thesis: verum end; hence contradiction by A16, A17, A18, SETFAM_1:def_1; ::_thesis: verum end; hence contradiction by A5; ::_thesis: verum end; then uparrow (fininfs xF) is proper by Th4; then consider GG being Filter of (BoolePoset the carrier of T) such that A23: uparrow (fininfs xF) c= GG and A24: GG is ultra by Th26; reconsider z = the Element of F as Subset of T by A9; A25: xF c= uparrow (fininfs xF) by WAYBEL_0:62; x \ z in xF by A6; then A26: x \ z in uparrow (fininfs xF) by A25; x \ z c= X ; then x in GG by A23, A26, Th7; then consider p being Element of T such that A27: p in y and A28: p is_a_convergence_point_of GG,T by A2, A24; consider W being set such that A29: p in W and A30: W in F by A4, A27, TARSKI:def_4; reconsider W = W as Subset of T by A30; W is open by A3, A30, TOPS_2:def_1; then A31: W in GG by A28, A29, Def5; A32: xF c= uparrow (fininfs xF) by WAYBEL_0:62; x \ W in xF by A30; then x \ W in uparrow (fininfs xF) by A32; then ( W misses x \ W & W /\ (x \ W) in GG ) by A23, A31, Th9, XBOOLE_1:79; then {} in GG by XBOOLE_0:def_7; then Bottom (BoolePoset the carrier of T) in GG by YELLOW_1:18; hence contradiction by A24, Th4; ::_thesis: verum end; theorem :: WAYBEL_7:31 for T being non empty TopSpace for B being prebasis of T for x, y being Element of (InclPoset the topology of T) st x c= y holds ( x << y iff for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) proof let T be non empty TopSpace; ::_thesis: for B being prebasis of T for x, y being Element of (InclPoset the topology of T) st x c= y holds ( x << y iff for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) let B be prebasis of T; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x c= y holds ( x << y iff for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) consider BB being Basis of T such that A1: BB c= FinMeetCl B by CANTOR_1:def_4; set BT = BoolePoset the carrier of T; set L = InclPoset the topology of T; let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x c= y implies ( x << y iff for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) ) assume A2: x c= y ; ::_thesis: ( x << y iff for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) A3: B c= the topology of T by TOPS_2:64; hereby ::_thesis: ( ( for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ) implies x << y ) assume A4: x << y ; ::_thesis: for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G let F be Subset of B; ::_thesis: ( y c= union F implies ex G being finite Subset of F st x c= union G ) assume A5: y c= union F ; ::_thesis: ex G being finite Subset of F st x c= union G reconsider FF = F as Subset-Family of T by XBOOLE_1:1; FF is open proof let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in FF or a is open ) assume a in FF ; ::_thesis: a is open then a in B ; hence a in the topology of T by A3; :: according to PRE_TOPC:def_2 ::_thesis: verum end; hence ex G being finite Subset of F st x c= union G by A4, A5, WAYBEL_3:34; ::_thesis: verum end; BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4; then A6: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1; InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1; then ( x in the topology of T & y in the topology of T ) ; then reconsider X = x, Y = y as Subset of T ; assume A7: for F being Subset of B st y c= union F holds ex G being finite Subset of F st x c= union G ; ::_thesis: x << y A8: the topology of T c= UniCl BB by CANTOR_1:def_2; now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_the_carrier_of_T)_st_x_in_F_holds_ ex_p_being_Element_of_T_st_ (_p_in_y_&_p_is_a_convergence_point_of_F,T_) deffunc H1( set ) -> Element of bool x = x \ $1; let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) assume that A9: x in F and A10: for p being Element of T holds ( not p in y or not p is_a_convergence_point_of F,T ) ; ::_thesis: contradiction defpred S1[ set , set ] means ( $1 in $2 & not $2 in F ); A11: now__::_thesis:_for_p_being_set_st_p_in_y_holds_ ex_r_being_set_st_ (_r_in_B_&_S1[p,r]_) let p be set ; ::_thesis: ( p in y implies ex r being set st ( r in B & S1[p,r] ) ) assume A12: p in y ; ::_thesis: ex r being set st ( r in B & S1[p,r] ) then p in Y ; then reconsider q = p as Element of T ; not q is_a_convergence_point_of F,T by A10, A12; then consider A being Subset of T such that A13: A is open and A14: q in A and A15: not A in F by Def5; A in the topology of T by A13, PRE_TOPC:def_2; then consider AY being Subset-Family of T such that A16: AY c= BB and A17: A = union AY by A8, CANTOR_1:def_1; consider ay being set such that A18: q in ay and A19: ay in AY by A14, A17, TARSKI:def_4; reconsider ay = ay as Subset of T by A19; ay in BB by A16, A19; then consider BY being Subset-Family of T such that A20: BY c= B and A21: BY is finite and A22: ay = Intersect BY by A1, CANTOR_1:def_3; ay c= A by A17, A19, ZFMISC_1:74; then not ay in F by A15, Th7; then BY is not Subset of F by A21, A22, Th11; then consider r being set such that A23: ( r in BY & not r in F ) by TARSKI:def_3; take r = r; ::_thesis: ( r in B & S1[p,r] ) thus ( r in B & S1[p,r] ) by A18, A20, A22, A23, SETFAM_1:43; ::_thesis: verum end; consider f being Function such that A24: ( dom f = y & rng f c= B ) and A25: for p being set st p in y holds S1[p,f . p] from FUNCT_1:sch_5(A11); reconsider FF = rng f as Subset of B by A24; y c= union FF proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y or p in union FF ) assume p in y ; ::_thesis: p in union FF then ( f . p in FF & p in f . p ) by A24, A25, FUNCT_1:def_3; hence p in union FF by TARSKI:def_4; ::_thesis: verum end; then consider G being finite Subset of FF such that A26: x c= union G by A7; set gg = the Element of G; consider g being Function such that A27: ( dom g = G & ( for z being set st z in G holds g . z = H1(z) ) ) from FUNCT_1:sch_3(); A28: rng g c= F proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in F ) A29: F is prime by Th22; assume a in rng g ; ::_thesis: a in F then consider b being set such that A30: b in G and A31: a = g . b by A27, FUNCT_1:def_3; b in FF by A30; then b in B ; then reconsider b = b as Subset of T ; ex p being set st ( p in y & b = f . p ) by A24, A30, FUNCT_1:def_3; then not b in F by A25; then A32: the carrier of T \ b in F by A29, Th21; a = x \ b by A27, A30, A31 .= X /\ (b `) by SUBSET_1:13 .= x /\ ( the carrier of T \ b) ; hence a in F by A9, A32, Th9; ::_thesis: verum end; then reconsider GG = rng g as finite Subset-Family of T by A6, A27, FINSET_1:8, XBOOLE_1:1; x <> Bottom (BoolePoset the carrier of T) by A9, Th4; then x <> {} by YELLOW_1:18; then A33: G <> {} by A26, ZFMISC_1:2; now__::_thesis:_for_a_being_set_holds_not_a_in_Intersect_GG let a be set ; ::_thesis: not a in Intersect GG assume A34: a in Intersect GG ; ::_thesis: contradiction now__::_thesis:_for_z_being_set_st_z_in_G_holds_ not_a_in_z let z be set ; ::_thesis: ( z in G implies not a in z ) assume z in G ; ::_thesis: not a in z then ( g . z in GG & g . z = x \ z ) by A27, FUNCT_1:def_3; then a in x \ z by A34, SETFAM_1:43; hence not a in z by XBOOLE_0:def_5; ::_thesis: verum end; then for z being set holds ( not a in z or not z in G ) ; then A35: not a in x by A26, TARSKI:def_4; ( g . the Element of G in GG & g . the Element of G = x \ the Element of G ) by A33, A27, FUNCT_1:def_3; then a in x \ the Element of G by A34, SETFAM_1:43; hence contradiction by A35; ::_thesis: verum end; then A36: Intersect GG = {} by XBOOLE_0:def_1; Intersect GG in F by A28, Th11; then Bottom (BoolePoset the carrier of T) in F by A36, YELLOW_1:18; hence contradiction by Th4; ::_thesis: verum end; hence x << y by A2, Th30; ::_thesis: verum end; theorem :: WAYBEL_7:32 for L being distributive complete LATTICE for x, y being Element of L holds ( x << y iff for P being prime Ideal of L st y <= sup P holds x in P ) proof let L be distributive complete LATTICE; ::_thesis: for x, y being Element of L holds ( x << y iff for P being prime Ideal of L st y <= sup P holds x in P ) let x, y be Element of L; ::_thesis: ( x << y iff for P being prime Ideal of L st y <= sup P holds x in P ) thus ( x << y implies for P being prime Ideal of L st y <= sup P holds x in P ) by WAYBEL_3:20; ::_thesis: ( ( for P being prime Ideal of L st y <= sup P holds x in P ) implies x << y ) assume A1: for P being prime Ideal of L st y <= sup P holds x in P ; ::_thesis: x << y now__::_thesis:_for_I_being_Ideal_of_L_st_y_<=_sup_I_holds_ x_in_I let I be Ideal of L; ::_thesis: ( y <= sup I implies x in I ) assume that A2: y <= sup I and A3: not x in I ; ::_thesis: contradiction consider P being Ideal of L such that A4: P is prime and A5: I c= P and A6: not x in P by A3, Th24; sup I <= sup P by A5, Th1; hence contradiction by A1, A2, A4, A6, ORDERS_2:3; ::_thesis: verum end; hence x << y by WAYBEL_3:21; ::_thesis: verum end; theorem Th33: :: WAYBEL_7:33 for L being LATTICE for p being Element of L st p is prime holds downarrow p is prime proof let L be LATTICE; ::_thesis: for p being Element of L st p is prime holds downarrow p is prime let p be Element of L; ::_thesis: ( p is prime implies downarrow p is prime ) assume A1: for x, y being Element of L holds ( not x "/\" y <= p or x <= p or y <= p ) ; :: according to WAYBEL_6:def_6 ::_thesis: downarrow p is prime let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in downarrow p or x in downarrow p or y in downarrow p ) assume x "/\" y in downarrow p ; ::_thesis: ( x in downarrow p or y in downarrow p ) then x "/\" y <= p by WAYBEL_0:17; then ( x <= p or y <= p ) by A1; hence ( x in downarrow p or y in downarrow p ) by WAYBEL_0:17; ::_thesis: verum end; begin definition let L be LATTICE; let p be Element of L; attrp is pseudoprime means :Def6: :: WAYBEL_7:def 6 ex P being prime Ideal of L st p = sup P; end; :: deftheorem Def6 defines pseudoprime WAYBEL_7:def_6_:_ for L being LATTICE for p being Element of L holds ( p is pseudoprime iff ex P being prime Ideal of L st p = sup P ); theorem Th34: :: WAYBEL_7:34 for L being LATTICE for p being Element of L st p is prime holds p is pseudoprime proof let L be LATTICE; ::_thesis: for p being Element of L st p is prime holds p is pseudoprime let p be Element of L; ::_thesis: ( p is prime implies p is pseudoprime ) assume p is prime ; ::_thesis: p is pseudoprime then A1: downarrow p is prime by Th33; p = sup (downarrow p) by WAYBEL_0:34; hence ex P being prime Ideal of L st p = sup P by A1; :: according to WAYBEL_7:def_6 ::_thesis: verum end; theorem Th35: :: WAYBEL_7:35 for L being continuous LATTICE for p being Element of L st p is pseudoprime holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) proof let L be continuous LATTICE; ::_thesis: for p being Element of L st p is pseudoprime holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) let p be Element of L; ::_thesis: ( p is pseudoprime implies for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) given P being prime Ideal of L such that A1: p = sup P ; :: according to WAYBEL_7:def_6 ::_thesis: for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) let A be non empty finite Subset of L; ::_thesis: ( inf A << p implies ex a being Element of L st ( a in A & a <= p ) ) assume inf A << p ; ::_thesis: ex a being Element of L st ( a in A & a <= p ) then A2: inf A in waybelow p ; waybelow p c= P by A1, WAYBEL_5:1; then consider a being Element of L such that A3: ( a in A & a in P ) by A2, Th12; take a ; ::_thesis: ( a in A & a <= p ) ex_sup_of P,L by WAYBEL_0:75; then P is_<=_than p by A1, YELLOW_0:30; hence ( a in A & a <= p ) by A3, LATTICE3:def_9; ::_thesis: verum end; theorem :: WAYBEL_7:36 for L being continuous LATTICE for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) holds uparrow (fininfs ((downarrow p) `)) misses waybelow p proof let L be continuous LATTICE; ::_thesis: for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) holds uparrow (fininfs ((downarrow p) `)) misses waybelow p let p be Element of L; ::_thesis: ( ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) implies uparrow (fininfs ((downarrow p) `)) misses waybelow p ) assume that A1: ( p <> Top L or not Top L is compact ) and A2: for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ; ::_thesis: uparrow (fininfs ((downarrow p) `)) misses waybelow p now__::_thesis:_for_x_being_set_st_x_in_uparrow_(fininfs_((downarrow_p)_`))_holds_ not_x_in_waybelow_p let x be set ; ::_thesis: ( x in uparrow (fininfs ((downarrow p) `)) implies not x in waybelow p ) assume A3: x in uparrow (fininfs ((downarrow p) `)) ; ::_thesis: not x in waybelow p then reconsider a = x as Element of L ; consider b being Element of L such that A4: a >= b and A5: b in fininfs ((downarrow p) `) by A3, WAYBEL_0:def_16; assume x in waybelow p ; ::_thesis: contradiction then A6: a << p by WAYBEL_3:7; then A7: b << p by A4, WAYBEL_3:2; consider Y being finite Subset of ((downarrow p) `) such that A8: b = "/\" (Y,L) and ex_inf_of Y,L by A5; reconsider Y = Y as finite Subset of L by XBOOLE_1:1; percases ( Y <> {} or Y = {} ) ; suppose Y <> {} ; ::_thesis: contradiction then consider c being Element of L such that A9: c in Y and A10: c <= p by A2, A4, A8, A6, WAYBEL_3:2; c in downarrow p by A10, WAYBEL_0:17; then ( downarrow p misses (downarrow p) ` & c in (downarrow p) /\ ((downarrow p) `) ) by A9, XBOOLE_0:def_4, XBOOLE_1:79; hence contradiction by XBOOLE_0:def_7; ::_thesis: verum end; supposeA11: Y = {} ; ::_thesis: contradiction ( b <= p & p <= Top L ) by A7, WAYBEL_3:1, YELLOW_0:45; then p = Top L by A8, A11, ORDERS_2:2; hence contradiction by A1, A8, A7, A11, WAYBEL_3:def_2; ::_thesis: verum end; end; end; hence uparrow (fininfs ((downarrow p) `)) misses waybelow p by XBOOLE_0:3; ::_thesis: verum end; theorem :: WAYBEL_7:37 for L being continuous LATTICE st Top L is compact holds ( ( for A being non empty finite Subset of L st inf A << Top L holds ex a being Element of L st ( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) proof let L be continuous LATTICE; ::_thesis: ( Top L is compact implies ( ( for A being non empty finite Subset of L st inf A << Top L holds ex a being Element of L st ( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) ) assume A1: Top L << Top L ; :: according to WAYBEL_3:def_2 ::_thesis: ( ( for A being non empty finite Subset of L st inf A << Top L holds ex a being Element of L st ( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) A2: now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_ (_x_in_uparrow_(fininfs_((downarrow_(Top_L))_`))_&_x_in_waybelow_(Top_L)_) take x = Top L; ::_thesis: ( x in uparrow (fininfs ((downarrow (Top L)) `)) & x in waybelow (Top L) ) thus x in uparrow (fininfs ((downarrow (Top L)) `)) by WAYBEL_4:22; ::_thesis: x in waybelow (Top L) thus x in waybelow (Top L) by A1; ::_thesis: verum end; hereby ::_thesis: uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) let A be non empty finite Subset of L; ::_thesis: ( inf A << Top L implies ex a being Element of L st ( a in A & a <= Top L ) ) assume inf A << Top L ; ::_thesis: ex a being Element of L st ( a in A & a <= Top L ) set a = the Element of A; reconsider a = the Element of A as Element of L ; take a = a; ::_thesis: ( a in A & a <= Top L ) thus ( a in A & a <= Top L ) by YELLOW_0:45; ::_thesis: verum end; thus uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) by A2, XBOOLE_0:3; ::_thesis: verum end; theorem :: WAYBEL_7:38 for L being continuous LATTICE for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) proof let L be continuous LATTICE; ::_thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) let p be Element of L; ::_thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) assume A1: uparrow (fininfs ((downarrow p) `)) misses waybelow p ; ::_thesis: for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) let A be non empty finite Subset of L; ::_thesis: ( inf A << p implies ex a being Element of L st ( a in A & a <= p ) ) assume inf A << p ; ::_thesis: ex a being Element of L st ( a in A & a <= p ) then inf A in waybelow p ; then not inf A in uparrow (fininfs ((downarrow p) `)) by A1, XBOOLE_0:3; then ( (downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) & not A c= uparrow (fininfs ((downarrow p) `)) ) by WAYBEL_0:43, WAYBEL_0:62; then not A c= (downarrow p) ` by XBOOLE_1:1; then consider a being set such that A2: a in A and A3: not a in (downarrow p) ` by TARSKI:def_3; reconsider a = a as Element of L by A2; take a ; ::_thesis: ( a in A & a <= p ) a in downarrow p by A3, SUBSET_1:29; hence ( a in A & a <= p ) by A2, WAYBEL_0:17; ::_thesis: verum end; theorem :: WAYBEL_7:39 for L being distributive continuous LATTICE for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds p is pseudoprime proof let L be distributive continuous LATTICE; ::_thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds p is pseudoprime let p be Element of L; ::_thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies p is pseudoprime ) set I = waybelow p; set F = uparrow (fininfs ((downarrow p) `)); A1: ( ex_sup_of downarrow p,L & sup (downarrow p) = p ) by WAYBEL_0:34; (downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) by WAYBEL_0:62; then A2: (uparrow (fininfs ((downarrow p) `))) ` c= ((downarrow p) `) ` by SUBSET_1:12; assume uparrow (fininfs ((downarrow p) `)) misses waybelow p ; ::_thesis: p is pseudoprime then consider P being Ideal of L such that A3: P is prime and A4: waybelow p c= P and A5: P misses uparrow (fininfs ((downarrow p) `)) by Th23; reconsider P = P as prime Ideal of L by A3; A6: ex_sup_of P,L by WAYBEL_0:75; ( ex_sup_of waybelow p,L & p = sup (waybelow p) ) by WAYBEL_0:75, WAYBEL_3:def_5; then A7: sup P >= p by A4, A6, YELLOW_0:34; take P ; :: according to WAYBEL_7:def_6 ::_thesis: p = sup P P c= (uparrow (fininfs ((downarrow p) `))) ` by A5, SUBSET_1:23; then sup P <= p by A6, A2, A1, XBOOLE_1:1, YELLOW_0:34; hence p = sup P by A7, ORDERS_2:2; ::_thesis: verum end; definition let L be non empty RelStr ; let R be Relation of the carrier of L; attrR is multiplicative means :Def7: :: WAYBEL_7:def 7 for a, x, y being Element of L st [a,x] in R & [a,y] in R holds [a,(x "/\" y)] in R; end; :: deftheorem Def7 defines multiplicative WAYBEL_7:def_7_:_ for L being non empty RelStr for R being Relation of the carrier of L holds ( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds [a,(x "/\" y)] in R ); registration let L be lower-bounded sup-Semilattice; let R be auxiliary Relation of L; let x be Element of L; clusterR -above x -> upper ; coherence R -above x is upper proof let y, z be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not y in R -above x or not y <= z or z in R -above x ) assume that A1: y in R -above x and A2: y <= z ; ::_thesis: z in R -above x ( x <= x & [x,y] in R ) by A1, WAYBEL_4:14; then [x,z] in R by A2, WAYBEL_4:def_4; hence z in R -above x by WAYBEL_4:14; ::_thesis: verum end; end; theorem :: WAYBEL_7:40 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff for x being Element of L holds R -above x is filtered ) proof let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds ( R is multiplicative iff for x being Element of L holds R -above x is filtered ) let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for x being Element of L holds R -above x is filtered ) hereby ::_thesis: ( ( for x being Element of L holds R -above x is filtered ) implies R is multiplicative ) assume A1: R is multiplicative ; ::_thesis: for x being Element of L holds R -above x is filtered let x be Element of L; ::_thesis: R -above x is filtered thus R -above x is filtered ::_thesis: verum proof let y, z be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not y in R -above x or not z in R -above x or ex b1 being Element of the carrier of L st ( b1 in R -above x & b1 <= y & b1 <= z ) ) assume ( y in R -above x & z in R -above x ) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in R -above x & b1 <= y & b1 <= z ) then ( [x,y] in R & [x,z] in R ) by WAYBEL_4:14; then [x,(y "/\" z)] in R by A1, Def7; then A2: y "/\" z in R -above x by WAYBEL_4:14; ( y >= y "/\" z & z >= y "/\" z ) by YELLOW_0:23; hence ex b1 being Element of the carrier of L st ( b1 in R -above x & b1 <= y & b1 <= z ) by A2; ::_thesis: verum end; end; assume A3: for x being Element of L holds R -above x is filtered ; ::_thesis: R is multiplicative let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R ) assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R then A4: ( x in R -above a & y in R -above a ) by WAYBEL_4:14; R -above a is filtered by A3; then x "/\" y in R -above a by A4, WAYBEL_0:41; hence [a,(x "/\" y)] in R by WAYBEL_4:14; ::_thesis: verum end; theorem Th41: :: WAYBEL_7:41 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R ) proof let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds ( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R ) let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R ) hereby ::_thesis: ( ( for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R ) implies R is multiplicative ) assume A1: R is multiplicative ; ::_thesis: for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R let a, b, x, y be Element of L; ::_thesis: ( [a,x] in R & [b,y] in R implies [(a "/\" b),(x "/\" y)] in R ) assume that A2: [a,x] in R and A3: [b,y] in R ; ::_thesis: [(a "/\" b),(x "/\" y)] in R ( a "/\" b <= b & y <= y ) by YELLOW_0:23; then A4: [(a "/\" b),y] in R by A3, WAYBEL_4:def_4; ( a >= a "/\" b & x <= x ) by YELLOW_0:23; then [(a "/\" b),x] in R by A2, WAYBEL_4:def_4; hence [(a "/\" b),(x "/\" y)] in R by A1, A4, Def7; ::_thesis: verum end; assume A5: for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds [(a "/\" b),(x "/\" y)] in R ; ::_thesis: R is multiplicative let a be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: for x, y being Element of L st [a,x] in R & [a,y] in R holds [a,(x "/\" y)] in R a "/\" a = a by YELLOW_0:25; hence for x, y being Element of L st [a,x] in R & [a,y] in R holds [a,(x "/\" y)] in R by A5; ::_thesis: verum end; theorem :: WAYBEL_7:42 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ) proof let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ) let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ) reconsider X = R as Subset of [:L,L:] by YELLOW_3:def_2; A1: X = the carrier of (subrelstr X) by YELLOW_0:def_15; hereby ::_thesis: ( ( for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ) implies R is multiplicative ) assume A2: R is multiplicative ; ::_thesis: for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting let S be full SubRelStr of [:L,L:]; ::_thesis: ( the carrier of S = R implies S is meet-inheriting ) assume A3: the carrier of S = R ; ::_thesis: S is meet-inheriting thus S is meet-inheriting ::_thesis: verum proof let x, y be Element of [:L,L:]; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) assume A4: ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2; then A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21; ex_inf_of {x,y},[:L,L:] by YELLOW_0:21; then inf {x,y} = [(inf (proj1 {x,y})),(inf (proj2 {x,y}))] by YELLOW_3:47 .= [(inf {(x `1),(y `1)}),(inf (proj2 {x,y}))] by A5, FUNCT_5:13 .= [(inf {(x `1),(y `1)}),(inf {(x `2),(y `2)})] by A5, FUNCT_5:13 .= [((x `1) "/\" (y `1)),(inf {(x `2),(y `2)})] by YELLOW_0:40 .= [((x `1) "/\" (y `1)),((x `2) "/\" (y `2))] by YELLOW_0:40 ; hence ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) by A2, A3, A4, A5, Th41; ::_thesis: verum end; end; assume for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ; ::_thesis: R is multiplicative then A6: subrelstr X is meet-inheriting by A1; let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R ) A7: ex_inf_of {[a,x],[a,y]},[:L,L:] by YELLOW_0:21; assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R then inf {[a,x],[a,y]} in R by A1, A6, A7, YELLOW_0:def_16; then A8: [a,x] "/\" [a,y] in R by YELLOW_0:40; set ax = [a,x]; set ay = [a,y]; [a,x] "/\" [a,y] = inf {[a,x],[a,y]} by YELLOW_0:40 .= [(inf (proj1 {[a,x],[a,y]})),(inf (proj2 {[a,x],[a,y]}))] by A7, YELLOW_3:47 .= [(inf {a,a}),(inf (proj2 {[a,x],[a,y]}))] by FUNCT_5:13 .= [(inf {a,a}),(inf {x,y})] by FUNCT_5:13 .= [(a "/\" a),(inf {x,y})] by YELLOW_0:40 .= [(a "/\" a),(x "/\" y)] by YELLOW_0:40 ; hence [a,(x "/\" y)] in R by A8, YELLOW_0:25; ::_thesis: verum end; theorem :: WAYBEL_7:43 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff R -below is meet-preserving ) proof let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds ( R is multiplicative iff R -below is meet-preserving ) let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff R -below is meet-preserving ) hereby ::_thesis: ( R -below is meet-preserving implies R is multiplicative ) assume A1: R is multiplicative ; ::_thesis: R -below is meet-preserving thus R -below is meet-preserving ::_thesis: verum proof let x, y be Element of L; :: according to WAYBEL_0:def_34 ::_thesis: R -below preserves_inf_of {x,y} A2: (R -below) . y = R -below y by WAYBEL_4:def_12; A3: R -below (x "/\" y) = (R -below x) /\ (R -below y) proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (R -below x) /\ (R -below y) c= R -below (x "/\" y) let a be set ; ::_thesis: ( a in R -below (x "/\" y) implies a in (R -below x) /\ (R -below y) ) assume a in R -below (x "/\" y) ; ::_thesis: a in (R -below x) /\ (R -below y) then a in { z where z is Element of L : [z,(x "/\" y)] in R } by WAYBEL_4:def_10; then consider z being Element of L such that A4: a = z and A5: [z,(x "/\" y)] in R ; A6: z <= z ; x "/\" y <= y by YELLOW_0:23; then [z,y] in R by A5, A6, WAYBEL_4:def_4; then A7: z in R -below y by WAYBEL_4:13; x "/\" y <= x by YELLOW_0:23; then [z,x] in R by A5, A6, WAYBEL_4:def_4; then z in R -below x by WAYBEL_4:13; hence a in (R -below x) /\ (R -below y) by A4, A7, XBOOLE_0:def_4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R -below x) /\ (R -below y) or a in R -below (x "/\" y) ) assume A8: a in (R -below x) /\ (R -below y) ; ::_thesis: a in R -below (x "/\" y) then reconsider z = a as Element of L ; a in R -below y by A8, XBOOLE_0:def_4; then A9: [z,y] in R by WAYBEL_4:13; a in R -below x by A8, XBOOLE_0:def_4; then [z,x] in R by WAYBEL_4:13; then [z,(x "/\" y)] in R by A1, A9, Def7; hence a in R -below (x "/\" y) by WAYBEL_4:13; ::_thesis: verum end; ( (R -below) . (x "/\" y) = R -below (x "/\" y) & (R -below) . x = R -below x ) by WAYBEL_4:def_12; then (R -below) . (x "/\" y) = ((R -below) . x) "/\" ((R -below) . y) by A2, A3, YELLOW_2:43; hence R -below preserves_inf_of {x,y} by YELLOW_3:8; ::_thesis: verum end; end; assume A10: for x, y being Element of L holds R -below preserves_inf_of {x,y} ; :: according to WAYBEL_0:def_34 ::_thesis: R is multiplicative let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R ) R -below preserves_inf_of {x,y} by A10; then A11: (R -below) . (x "/\" y) = ((R -below) . x) "/\" ((R -below) . y) by YELLOW_3:8 .= ((R -below) . x) /\ ((R -below) . y) by YELLOW_2:43 ; A12: (R -below) . y = R -below y by WAYBEL_4:def_12; assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R then A13: ( a in R -below x & a in R -below y ) by WAYBEL_4:13; ( (R -below) . (x "/\" y) = R -below (x "/\" y) & (R -below) . x = R -below x ) by WAYBEL_4:def_12; then a in R -below (x "/\" y) by A11, A12, A13, XBOOLE_0:def_4; hence [a,(x "/\" y)] in R by WAYBEL_4:13; ::_thesis: verum end; Lm3: now__::_thesis:_for_L_being_lower-bounded_continuous_LATTICE for_p_being_Element_of_L_st_L_-waybelow_is_multiplicative_&_(_for_a,_b_being_Element_of_L_holds_ (_not_a_"/\"_b_<<_p_or_a_<=_p_or_b_<=_p_)_)_holds_ p_is_prime let L be lower-bounded continuous LATTICE; ::_thesis: for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) holds p is prime let p be Element of L; ::_thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime ) assume that A1: L -waybelow is multiplicative and A2: for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) and A3: not p is prime ; ::_thesis: contradiction consider x, y being Element of L such that A4: x "/\" y <= p and A5: not x <= p and A6: not y <= p by A3, WAYBEL_6:def_6; A7: for a being Element of L holds ( not waybelow a is empty & waybelow a is directed ) ; then consider u being Element of L such that A8: u << x and A9: not u <= p by A5, WAYBEL_3:24; consider v being Element of L such that A10: v << y and A11: not v <= p by A6, A7, WAYBEL_3:24; A12: [v,y] in L -waybelow by A10, WAYBEL_4:def_1; [u,x] in L -waybelow by A8, WAYBEL_4:def_1; then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, A12, Th41; then u "/\" v << x "/\" y by WAYBEL_4:def_1; then u "/\" v << p by A4, WAYBEL_3:2; hence contradiction by A2, A9, A11; ::_thesis: verum end; theorem Th44: :: WAYBEL_7:44 for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds for p being Element of L holds ( p is pseudoprime iff for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) proof let L be lower-bounded continuous LATTICE; ::_thesis: ( L -waybelow is multiplicative implies for p being Element of L holds ( p is pseudoprime iff for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) ) assume A1: L -waybelow is multiplicative ; ::_thesis: for p being Element of L holds ( p is pseudoprime iff for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) let p be Element of L; ::_thesis: ( p is pseudoprime iff for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) hereby ::_thesis: ( ( for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) implies p is pseudoprime ) assume A2: p is pseudoprime ; ::_thesis: for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) let a, b be Element of L; ::_thesis: ( not a "/\" b << p or a <= p or b <= p ) assume a "/\" b << p ; ::_thesis: ( a <= p or b <= p ) then inf {a,b} << p by YELLOW_0:40; then ex c being Element of L st ( c in {a,b} & c <= p ) by A2, Th35; hence ( a <= p or b <= p ) by TARSKI:def_2; ::_thesis: verum end; assume for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ; ::_thesis: p is pseudoprime hence p is pseudoprime by A1, Lm3, Th34; ::_thesis: verum end; theorem :: WAYBEL_7:45 for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds for p being Element of L st p is pseudoprime holds p is prime proof let L be lower-bounded continuous LATTICE; ::_thesis: ( L -waybelow is multiplicative implies for p being Element of L st p is pseudoprime holds p is prime ) assume A1: L -waybelow is multiplicative ; ::_thesis: for p being Element of L st p is pseudoprime holds p is prime let p be Element of L; ::_thesis: ( p is pseudoprime implies p is prime ) assume p is pseudoprime ; ::_thesis: p is prime then for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) by A1, Th44; hence p is prime by A1, Lm3; ::_thesis: verum end; theorem :: WAYBEL_7:46 for L being lower-bounded distributive continuous LATTICE st ( for p being Element of L st p is pseudoprime holds p is prime ) holds L -waybelow is multiplicative proof let L be lower-bounded distributive continuous LATTICE; ::_thesis: ( ( for p being Element of L st p is pseudoprime holds p is prime ) implies L -waybelow is multiplicative ) assume A1: for p being Element of L st p is pseudoprime holds p is prime ; ::_thesis: L -waybelow is multiplicative given a, x, y being Element of L such that A2: ( [a,x] in L -waybelow & [a,y] in L -waybelow ) and A3: not [a,(x "/\" y)] in L -waybelow ; :: according to WAYBEL_7:def_7 ::_thesis: contradiction now__::_thesis:_for_z_being_set_st_z_in_waybelow_(x_"/\"_y)_holds_ not_z_in_uparrow_a let z be set ; ::_thesis: ( z in waybelow (x "/\" y) implies not z in uparrow a ) assume that A4: z in waybelow (x "/\" y) and A5: z in uparrow a ; ::_thesis: contradiction reconsider z = z as Element of L by A4; ( z << x "/\" y & z >= a ) by A4, A5, WAYBEL_0:18, WAYBEL_3:7; then a << x "/\" y by WAYBEL_3:2; hence contradiction by A3, WAYBEL_4:def_1; ::_thesis: verum end; then waybelow (x "/\" y) misses uparrow a by XBOOLE_0:3; then consider P being Ideal of L such that A6: P is prime and A7: waybelow (x "/\" y) c= P and A8: P misses uparrow a by Th23; set p = sup P; sup P is pseudoprime by A6, Def6; then A9: sup P is prime by A1; a <= a ; then A10: a in uparrow a by WAYBEL_0:18; A11: ( x "/\" y = sup (waybelow (x "/\" y)) & ex_sup_of waybelow (x "/\" y),L ) by WAYBEL_0:75, WAYBEL_3:def_5; ex_sup_of P,L by WAYBEL_0:75; then x "/\" y <= sup P by A7, A11, YELLOW_0:34; then ( ( x <= sup P & a << x ) or ( y <= sup P & a << y ) ) by A2, A9, WAYBEL_4:def_1, WAYBEL_6:def_6; then a in P by WAYBEL_3:20; hence contradiction by A8, A10, XBOOLE_0:3; ::_thesis: verum end;