waybel_7.miz

    begin

    theorem :: WAYBEL_7:1



     Th1: for L be complete LATTICE, X,Y be set st X c= Y holds ( "\/" (X,L)) <= ( "\/" (Y,L)) & ( "/\" (X,L)) >= ( "/\" (Y,L))

    proof

      let L be complete LATTICE, X,Y be set;



       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 thesis by A1, YELLOW_0: 34, YELLOW_0: 35;

    end;

    theorem :: WAYBEL_7:2



     Th2: for X be set holds the carrier of ( BoolePoset X) = ( bool X)

    proof

      let X be set;

      set L = ( BoolePoset X);

      L = ( InclPoset ( bool X)) by YELLOW_1: 4;

      then L = RelStr (# ( bool X), ( RelIncl ( bool X)) #) by YELLOW_1:def 1;

      hence thesis;

    end;

    theorem :: WAYBEL_7:3

    for L be bounded antisymmetric non empty RelStr holds L is trivial iff ( Top L) = ( Bottom L)

    proof

      let L be bounded antisymmetric non empty RelStr;

      thus L is trivial implies ( Top L) = ( Bottom L);

      assume

       A1: ( Top L) = ( Bottom L);

      let x,y be Element of L;

      reconsider x, 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 thesis by A2, ORDERS_2: 2;

    end;

    registration

      let X be set;

      cluster ( BoolePoset X) -> Boolean;

      coherence ;

    end

    registration

      let X be non empty set;

      cluster ( BoolePoset X) -> non trivial;

      coherence

      proof

        ( Top ( BoolePoset X)) = X & ( Bottom ( BoolePoset X)) = {} by YELLOW_1: 18, YELLOW_1: 19;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_7:4



     Th4: for L be lower-bounded non empty Poset, F be Filter of L holds F is proper iff not ( Bottom L) in F

    proof

      let L be lower-bounded non empty Poset, F be Filter of L;

      hereby

        assume F is proper;

        then F <> the carrier of L;

        then

        consider a be object such that

         A1: not (a in F iff a in the carrier of L) by TARSKI: 2;

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

      end;

      assume not ( Bottom L) in F;

      then F <> the carrier of L;

      hence thesis;

    end;

    registration

      cluster non trivial Boolean strict for LATTICE;

      existence

      proof

        take ( BoolePoset { {} });

        thus thesis;

      end;

    end

    registration

      let L be upper-bounded non trivial Poset;

      cluster proper for Filter of L;

      existence

      proof

        take F = ( uparrow ( Top L));

        assume not F is proper;

        then

         A1: F = the carrier of L;

        now

          let x,y be Element of L;



           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;

        end;

        hence thesis by STRUCT_0:def 10;

      end;

    end

    theorem :: WAYBEL_7:5



     Th5: for X be set, a be Element of ( BoolePoset X) holds ( 'not' a) = (X \ a)

    proof

      let X be set, a be Element of ( BoolePoset X);



       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

      .= ( 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 thesis by YELLOW_5: 11;

    end;

    theorem :: WAYBEL_7:6

    for X be set, Y be Subset of ( BoolePoset X) holds Y is lower iff for x,y be set st x c= y & y in Y holds x in Y

    proof

      let X be set, Y be Subset of ( BoolePoset X);



       A1: the carrier of ( BoolePoset X) = ( bool X) by Th2;

      hereby

        assume

         A2: Y is lower;

        let x,y be set;

        assume that

         A3: x c= y and

         A4: y 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;

      end;

      assume

       A5: for x,y be set st x c= y & y in Y holds x in Y;

      let a,b be Element of ( BoolePoset X);

      assume that

       A6: a in Y and

       A7: b <= a;

      b c= a by A7, YELLOW_1: 2;

      hence thesis by A5, A6;

    end;

    theorem :: WAYBEL_7:7



     Th7: for X be set, Y be Subset of ( BoolePoset X) holds Y is upper iff for x,y be set st x c= y & y c= X & x in Y holds y in Y

    proof

      let X be set, Y be Subset of ( BoolePoset X);



       A1: the carrier of ( BoolePoset X) = ( bool X) by Th2;

      hereby

        assume

         A2: Y is upper;

        let x,y be set;

        assume that

         A3: x c= y and

         A4: y c= X and

         A5: x 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;

      end;

      assume

       A6: for x,y be set st x c= y & y c= X & x in Y holds y in Y;

      let a,b be Element of ( BoolePoset X);

      assume that

       A7: a in Y and

       A8: b >= a;

      a c= b by A8, YELLOW_1: 2;

      hence thesis by A1, A6, A7;

    end;

    theorem :: WAYBEL_7:8

    for X be set, Y be lower Subset of ( BoolePoset X) holds Y is directed iff for x,y be set st x in Y & y in Y holds (x \/ y) in Y

    proof

      let X be set, Y be lower Subset of ( BoolePoset X);

      hereby

        assume

         A1: Y is directed;

        let x,y be set;

        assume

         A2: x in Y & 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;

      end;

      assume

       A3: for x,y be set st x in Y & y in Y holds (x \/ y) in Y;

      now

        let a,b be Element of ( BoolePoset X);

        assume a in Y & b in Y;

        then (a \/ b) in Y by A3;

        hence (a "\/" b) in Y by YELLOW_1: 17;

      end;

      hence thesis by WAYBEL_0: 40;

    end;

    theorem :: WAYBEL_7:9



     Th9: for X be set, Y be upper Subset of ( BoolePoset X) holds Y is filtered iff for x,y be set st x in Y & y in Y holds (x /\ y) in Y

    proof

      let X be set, Y be upper Subset of ( BoolePoset X);

      hereby

        assume

         A1: Y is filtered;

        let x,y be set;

        assume

         A2: x in Y & 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;

      end;

      assume

       A3: for x,y be set st x in Y & y in Y holds (x /\ y) in Y;

      now

        let a,b be Element of ( BoolePoset X);

        assume a in Y & b in Y;

        then (a /\ b) in Y by A3;

        hence (a "/\" b) in Y by YELLOW_1: 17;

      end;

      hence thesis by WAYBEL_0: 41;

    end;

    theorem :: WAYBEL_7:10

    for X be set, Y be non empty lower Subset of ( BoolePoset X) holds Y is directed iff for Z be finite Subset-Family of X st Z c= Y holds ( union Z) in Y

    proof

      let X be set, Y be non empty lower Subset of ( BoolePoset X);

      hereby

        assume

         A1: Y is directed;

        let Z be finite Subset-Family of X;

        reconsider B = Z as Subset of ( BoolePoset X) by Th2;

        assume Z c= 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;

      end;

      assume

       A3: for Z be finite Subset-Family of X st Z c= Y holds ( union Z) in Y;



       A4: the carrier of ( BoolePoset X) = ( bool X) by Th2;

      now

        let A be finite Subset of Y;

        reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1: 1;

        assume A <> {} ;

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

      end;

      hence thesis by WAYBEL_0: 42;

    end;

    theorem :: WAYBEL_7:11



     Th11: for X be set, Y be non empty upper Subset of ( BoolePoset X) holds Y is filtered iff for Z be finite Subset-Family of X st Z c= Y holds ( Intersect Z) in Y

    proof

      let X be set, Y be non empty upper Subset of ( BoolePoset X);

      hereby

        assume

         A1: Y is filtered;

        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;

        reconsider B = Z as Subset of ( BoolePoset X) by Th2;

        assume Z c= 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;

      end;

      assume

       A3: for Z be finite Subset-Family of X st Z c= Y holds ( Intersect Z) in Y;



       A4: the carrier of ( BoolePoset X) = ( bool X) by Th2;

      now

        let A be finite Subset of Y;

        reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1: 1;

        assume

         A5: A <> {} ;

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

      end;

      hence thesis by WAYBEL_0: 43;

    end;

    begin

    definition

      let L be with_infima Poset;

      let I be Ideal of L;

      :: WAYBEL_7:def1

      attr I is prime means

      : Def1: for x,y be Element of L st (x "/\" y) in I holds x in I or y in I;

    end

    theorem :: WAYBEL_7:12



     Th12: for L be with_infima Poset, I be Ideal of L holds I is prime iff for A be finite non empty Subset of L st ( inf A) in I holds ex a be Element of L st a in A & a in I

    proof

      let L be with_infima Poset, I be Ideal of L;

      thus I is prime implies for A be finite non empty Subset of L st ( inf A) in I holds ex a be Element of L st a in A & a in I

      proof

        defpred P[ set] means $1 is non empty & ( "/\" ($1,L)) in I implies ex a be Element of L st a in $1 & a in I;

        assume

         A1: for x,y be Element of L st (x "/\" y) in I holds x in I or y in I;

        let A be finite non empty Subset of L;

         A2:

        now

          let x,B be set such that

           A3: x in A and

           A4: B c= A and

           A5: P[B];

          thus P[(B \/ {x})]

          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 (B \/ {x}) is non empty and

             A6: ( "/\" ((B \/ {x}),L)) in I;

            per cases ;

              suppose B = {} ;

              then ( "/\" ((B \/ {a}),L)) = a & a in (B \/ {a}) by TARSKI:def 1, YELLOW_0: 39;

              hence thesis by A6;

            end;

              suppose

               A7: B <> {} ;



               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

                per cases by A1, A6, A10, A8;

                  suppose ( inf C) in I;

                  then

                  consider b be Element of L such that

                   A11: b in B & b in I by A5, A7;

                  take b;

                  thus b in (B \/ {x}) & b in I by A11, XBOOLE_0:def 3;

                end;

                  suppose

                   A12: a in I;

                  take a;

                  a in {a} by TARSKI:def 1;

                  hence a in (B \/ {x}) & a in I by A12, XBOOLE_0:def 3;

                end;

              end;

            end;

          end;

        end;



         A13: P[ {} ];



         A14: A is finite;

         P[A] from FINSET_1:sch 2( A14, A13, A2);

        hence thesis;

      end;

      assume

       A15: for A be finite non empty Subset of L st ( inf A) in I holds ex a be Element of L st a in A & a in I;

      let a,b be Element of L;

      assume (a "/\" b) in I;

      then ( inf {a, b}) in I by YELLOW_0: 40;

      then ex x be Element of L st x in {a, b} & x in I by A15;

      hence thesis by TARSKI:def 2;

    end;

    registration

      let L be LATTICE;

      cluster prime for Ideal of L;

      existence

      proof

        take ( [#] L);

        let x,y be Element of L;

        thus thesis;

      end;

    end

    theorem :: WAYBEL_7:13

    for L1,L2 be LATTICE st the RelStr of L1 = the RelStr of L2 holds for x be set st x is prime Ideal of L1 holds x is prime Ideal of L2

    proof

      let L1,L2 be LATTICE such that

       A1: the RelStr of L1 = the RelStr of L2;

      let x be set;

      assume x is prime Ideal of L1;

      then

      reconsider I = x as prime Ideal of L1;

      reconsider I9 = I as Subset of L2 by A1;

      reconsider I9 as Ideal of L2 by A1, WAYBEL_0: 3, WAYBEL_0: 25;

      I9 is prime

      proof

        let x,y be Element of L2;

        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 thesis by Def1;

      end;

      hence thesis;

    end;

    definition

      let L be with_suprema Poset;

      let F be Filter of L;

      :: WAYBEL_7:def2

      attr F is prime means

      : Def2: for x,y be Element of L st (x "\/" y) in F holds x in F or y in F;

    end

    theorem :: WAYBEL_7:14

    for L be with_suprema Poset, F be Filter of L holds F is prime iff for A be finite non empty Subset of L st ( sup A) in F holds ex a be Element of L st a in A & a in F

    proof

      let L be with_suprema Poset, I be Filter of L;

      thus I is prime implies for A be finite non empty Subset of L st ( sup A) in I holds ex a be Element of L st a in A & a in I

      proof

        defpred P[ set] means $1 is non empty & ( "\/" ($1,L)) in I implies ex a be Element of L st a in $1 & a in I;

        assume

         A1: for x,y be Element of L st (x "\/" y) in I holds x in I or y in I;

        let A be finite non empty Subset of L;

         A2:

        now

          let x,B be set such that

           A3: x in A and

           A4: B c= A and

           A5: P[B];

          thus P[(B \/ {x})]

          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 (B \/ {x}) is non empty and

             A6: ( "\/" ((B \/ {x}),L)) in I;

            per cases ;

              suppose B = {} ;

              then ( "\/" ((B \/ {a}),L)) = a & a in (B \/ {a}) by TARSKI:def 1, YELLOW_0: 39;

              hence thesis by A6;

            end;

              suppose

               A7: B <> {} ;



               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

                per cases by A1, A6, A10, A8;

                  suppose ( sup C) in I;

                  then

                  consider b be Element of L such that

                   A11: b in B & b in I by A5, A7;

                  take b;

                  thus b in (B \/ {x}) & b in I by A11, XBOOLE_0:def 3;

                end;

                  suppose

                   A12: a in I;

                  take a;

                  a in {a} by TARSKI:def 1;

                  hence a in (B \/ {x}) & a in I by A12, XBOOLE_0:def 3;

                end;

              end;

            end;

          end;

        end;



         A13: P[ {} ];



         A14: A is finite;

         P[A] from FINSET_1:sch 2( A14, A13, A2);

        hence thesis;

      end;

      assume

       A15: for A be finite non empty Subset of L st ( sup A) in I holds ex a be Element of L st a in A & a in I;

      let a,b be Element of L;

      assume (a "\/" b) in I;

      then ( sup {a, b}) in I by YELLOW_0: 41;

      then ex x be Element of L st x in {a, b} & x in I by A15;

      hence thesis by TARSKI:def 2;

    end;

    registration

      let L be LATTICE;

      cluster prime for Filter of L;

      existence

      proof

        take ( [#] L);

        let x,y be Element of L;

        thus thesis;

      end;

    end

    theorem :: WAYBEL_7:15



     Th15: for L1,L2 be LATTICE st the RelStr of L1 = the RelStr of L2 holds for x be set st x is prime Filter of L1 holds x is prime Filter of L2

    proof

      let L1,L2 be LATTICE such that

       A1: the RelStr of L1 = the RelStr of L2;

      let x be set;

      assume x is prime Filter of L1;

      then

      reconsider I = x as prime Filter of L1;

      reconsider I9 = I as Subset of L2 by A1;

      reconsider I9 as Filter of L2 by A1, WAYBEL_0: 4, WAYBEL_0: 25;

      I9 is prime

      proof

        let x,y be Element of L2;

        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 thesis by Def2;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_7:16



     Th16: for L be LATTICE, x be set holds x is prime Ideal of L iff x is prime Filter of (L opp )

    proof

      let L be LATTICE, x be set;

      hereby

        assume x is prime Ideal of L;

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



           A1: (x "\/" y) = (( ~ x) "/\" ( ~ y)) by YELLOW_7: 22;

          ( ~ x) = x & ( ~ y) = y by LATTICE3:def 7;

          hence thesis by A1, Def1;

        end;

        hence x is prime Filter of (L opp );

      end;

      assume x is prime Filter of (L opp );

      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;



         A2: (x "/\" y) = ((x ~ ) "\/" (y ~ )) by YELLOW_7: 21;

        (x ~ ) = x & (y ~ ) = y by LATTICE3:def 6;

        hence thesis by A2, Def2;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_7:17



     Th17: for L be LATTICE, x be set holds x is prime Filter of L iff x is prime Ideal of (L opp )

    proof

      let L be LATTICE, x be set;

      ((L opp ) opp ) = the RelStr of L by LATTICE3: 8;

      then x is prime Filter of L iff x is prime Filter of ((L opp ) opp ) by Th15;

      hence thesis by Th16;

    end;

    theorem :: WAYBEL_7:18

    for L be with_infima Poset, I be Ideal of L holds I is prime iff (I ` ) is Filter of L or (I ` ) = {}

    proof

      let L be with_infima Poset, I be Ideal of L;

      set F = (I ` );

      thus I is prime implies (I ` ) is Filter of L or (I ` ) = {}

      proof

        assume

         A1: for x,y be Element of L st (x "/\" y) in I holds x in I or y in I;



         A2: F is filtered

        proof

          let x,y be Element of L;

          assume x in F & y in F;

          then ( not x in I) & not y in I by XBOOLE_0:def 5;

          then

           A3: (x "/\" y) in F by A1, SUBSET_1: 29;

          (x "/\" y) <= x & (x "/\" y) <= y by YELLOW_0: 23;

          hence thesis by A3;

        end;

        F is upper

        proof

          let x,y be Element of L;

          assume that

           A4: x in F and

           A5: y >= x;

          y in I implies x in I by A5, WAYBEL_0:def 19;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

        hence thesis by A2;

      end;

      assume

       A6: (I ` ) is Filter of L or (I ` ) = {} ;

      let x,y be Element of L;

      assume (x "/\" y) in I;

      then not (x "/\" y) in F by XBOOLE_0:def 5;

      then not x in F or not y in F by A6, WAYBEL_0: 41;

      hence thesis by SUBSET_1: 29;

    end;

    theorem :: WAYBEL_7:19

    for L be LATTICE, I be Ideal of L holds I is prime iff I in ( PRIME ( InclPoset ( Ids L)))

    proof

      let L be LATTICE, I be Ideal of L;

      set P = ( InclPoset ( Ids L));



       A1: P = 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)))

      proof

        assume

         A2: for x,y be Element of L st (x "/\" y) in I holds x in I or y in I;

        i is prime

        proof

          let x,y be Element of P;

          y in ( Ids L) by A1;

          then

           A3: ex J be Ideal of L st y = J;

          x in ( Ids L) by A1;

          then ex J be Ideal of L st x = J;

          then

          reconsider X = x, Y = y as Ideal of L by A3;

          assume (x "/\" 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;

           not X c= I by A5, YELLOW_1: 3;

          then

          consider a be object such that

           A7: a in X and

           A8: not a in I;

           not Y c= I by A6, YELLOW_1: 3;

          then

          consider b be object such that

           A9: b in Y and

           A10: not b in I;

          reconsider a, 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 thesis by A2, A4, A8, A10;

        end;

        hence thesis by WAYBEL_6:def 7;

      end;

      assume

       A12: I in ( PRIME P);

      let x,y be Element of L;

      reconsider X = ( downarrow x), Y = ( downarrow y) as Ideal of L;

      X in ( Ids L) & Y in ( Ids L);

      then

      reconsider X, Y as Element of P by A1;



       A13: (X /\ Y) = (X "/\" Y) by YELLOW_2: 43;

      assume

       A14: (x "/\" y) in I;

      (X "/\" Y) c= I

      proof

        let a be object;

        assume

         A15: a in (X "/\" Y);

        then

         A16: a in X by A13, XBOOLE_0:def 4;



         A17: a in Y by A13, A15, XBOOLE_0:def 4;

        reconsider 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 thesis by A14, WAYBEL_0:def 19;

      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;

      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 thesis by A21, A20;

    end;

    theorem :: WAYBEL_7:20



     Th20: for L be Boolean LATTICE, F be Filter of L holds F is prime iff for a be Element of L holds a in F or ( 'not' a) in F

    proof

      let L be Boolean LATTICE;

      let F be Filter of L;

      hereby

        assume

         A1: F is prime;

        let a be Element of L;

        set b = ( 'not' a);

        (a "\/" b) = ( Top L) by YELLOW_5: 34;

        then (a "\/" b) in F by WAYBEL_4: 22;

        hence a in F or b in F by A1;

      end;

      assume

       A2: for a be Element of L holds a in F or ( 'not' a) in F;

      let a,b be Element of L;

      assume that

       A3: (a "\/" b) in F and

       A4: not a in F and

       A5: not b in F;

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

    end;

    theorem :: WAYBEL_7:21



     Th21: for X be set, F be Filter of ( BoolePoset X) holds F is prime iff for A be Subset of X holds A in F or (X \ A) in F

    proof

      let X be set;

      set L = ( BoolePoset X);

      let F be Filter of L;

      L = ( InclPoset ( bool X)) by YELLOW_1: 4;

      then

       A1: L = RelStr (# ( bool X), ( RelIncl ( bool X)) #) by YELLOW_1:def 1;

      hereby

        assume

         A2: F is prime;

        let A be Subset of X;

        reconsider a = A as Element of L by A1;

        a in F or ( 'not' a) in F by A2, Th20;

        hence A in F or (X \ A) in F by Th5;

      end;

      assume

       A3: for A be Subset of X holds A in F or (X \ A) in F;

      now

        let a be Element of L;

        ( 'not' a) = (X \ a) by Th5;

        hence a in F or ( 'not' a) in F by A1, A3;

      end;

      hence thesis by Th20;

    end;

    definition

      let L be non empty Poset;

      let F be Filter of L;

      :: WAYBEL_7:def3

      attr F is ultra means F is proper & for G be Filter of L st F c= G holds F = G or G = the carrier of L;

    end

    registration

      let L be non empty Poset;

      cluster ultra -> proper for Filter of L;

      coherence ;

    end



     Lm1: for L be with_infima Poset holds for F be Filter of L, X be finite non empty Subset of L holds for x be Element of L st x in ( uparrow ( fininfs (F \/ X))) holds ex a be Element of L st a in F & x >= (a "/\" ( inf X))

    proof

      let L be with_infima Poset;

      let I be Filter of L, X be finite non empty Subset of L;

      let x be Element of L;

      set i = the Element of I;

      reconsider i as Element of L;

      assume x in ( uparrow ( fininfs (I \/ X)));

      then

      consider u be Element of L such that

       A1: u <= x and

       A2: u in ( fininfs (I \/ X)) by WAYBEL_0:def 16;

      consider Y be 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 object;

        assume

         A5: a in (Y \ X);

        then not a in X by XBOOLE_0:def 5;

        hence thesis by A5, XBOOLE_0:def 3;

      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;

      per cases ;

        suppose

         A6: Z = {} ;



         A7: ( inf X) >= (i "/\" ( inf X)) by YELLOW_0: 23;

        take i;



         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 thesis by A1, ORDERS_2: 3;

      end;

        suppose

         A9: Z <> {} ;

        take ( inf Z9);



         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 thesis by A1, A3, A9, A12, ORDERS_2: 3, WAYBEL_0: 43;

      end;

    end;

    theorem :: WAYBEL_7:22



     Th22: for L be Boolean LATTICE, F be Filter of L holds F is proper prime iff F is ultra

    proof

      let L be Boolean LATTICE;

      let F be Filter of L;

      thus F is proper prime implies F is ultra

      proof

        assume

         A1: F is proper;

        assume

         A2: for x,y be Element of L st (x "\/" y) in F holds x in F or y in F;

        thus F is proper by A1;

        let G be Filter of L;

        assume that

         A3: F c= G and

         A4: F <> G;

        consider x be object such that

         A5: not (x in F iff x in G) by A4, TARSKI: 2;

        reconsider x as Element of L by A5;

        set y = ( 'not' x);

        (x "\/" y) = ( Top L) by YELLOW_5: 34;

        then y in F by A2, A3, A5, WAYBEL_4: 22;

        then (x "/\" y) 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;

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x as Element of L;

        x >= ( Bottom L) by YELLOW_0: 44;

        hence thesis by A6, WAYBEL_0:def 20;

      end;

      assume that

       A7: F is proper and

       A8: for G be Filter of L st F c= G holds F = G or G = the carrier of L;

      thus F is proper by A7;

      now

        let a be Element of L;

        assume that

         A9: not a in F and

         A10: not ( 'not' a) in F;

        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 be Element of L such that

         A12: c in F and

         A13: b >= (c "/\" ( inf {a})) by Lm1;

        c <= ( Top L) by YELLOW_0: 45;



        then

         A14: c = (c "/\" ( Top L)) by YELLOW_0: 25

        .= (c "/\" (a "\/" b)) by YELLOW_5: 34

        .= ((c "/\" a) "\/" (c "/\" b)) by WAYBEL_1:def 3;

        ( inf {a}) = a & (c "/\" b) <= b by YELLOW_0: 23, YELLOW_0: 39;

        then c <= b by A13, A14, YELLOW_0: 22;

        hence contradiction by A10, A12, WAYBEL_0:def 20;

      end;

      hence thesis by Th20;

    end;



     Lm2: for L be with_suprema Poset holds for I be Ideal of L, X be finite non empty Subset of L holds for x be Element of L st x in ( downarrow ( finsups (I \/ X))) holds ex i be Element of L st i in I & x <= (i "\/" ( sup X))

    proof

      let L be with_suprema Poset;

      let I be Ideal of L, X be finite non empty Subset of L;

      let x be Element of L;

      set i = the Element of I;

      reconsider i as Element of L;

      assume x in ( downarrow ( finsups (I \/ X)));

      then

      consider u be Element of L such that

       A1: u >= x and

       A2: u in ( finsups (I \/ X)) by WAYBEL_0:def 15;

      consider Y be 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 object;

        assume

         A5: a in (Y \ X);

        then not a in X by XBOOLE_0:def 5;

        hence thesis by A5, XBOOLE_0:def 3;

      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;

      per cases ;

        suppose

         A6: Z = {} ;



         A7: ( sup X) <= (i "\/" ( sup X)) by YELLOW_0: 22;

        take i;



         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 thesis by A1, ORDERS_2: 3;

      end;

        suppose

         A9: Z <> {} ;

        take ( sup Z9);



         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 thesis by A1, A3, A9, A12, ORDERS_2: 3, WAYBEL_0: 42;

      end;

    end;

    theorem :: WAYBEL_7:23



     Th23: for L be distributive LATTICE, I be Ideal of L, F be Filter of L st I misses F holds ex P be Ideal of L st P is prime & I c= P & P misses F

    proof

      let L be distributive LATTICE, I be Ideal of L, F be Filter of L such that

       A1: I misses F;

      set X = { P where P be Ideal of L : I c= P & P misses F };

       A2:

      now

        let A be set;

        assume A in X;

        then ex P be Ideal of L st A = P & I c= P & P misses F;

        hence I c= A & A misses F;

      end;

       A3:

      now

        let Z be set such that

         A4: Z <> {} and

         A5: Z c= X and

         A6: Z is c=-linear;

        Z c= ( bool the carrier of L)

        proof

          let x be object;

          assume x in Z;

          then x in X by A5;

          then ex P be Ideal of L st x = P & I c= P & P misses F;

          hence thesis;

        end;

        then

        reconsider ZI = Z as Subset-Family of L;

        now

          let A be Subset of L;

          assume A in ZI;

          then A in X by A5;

          then ex P be Ideal of L st A = P & I c= P & P misses F;

          hence A is lower;

        end;

        then

        reconsider J = ( union ZI) as lower Subset of L by WAYBEL_0: 26;

         A7:

        now

          set y = the Element of Z;

          y in Z by A4;

          then

           A8: I c= y by A2, A5;



           A9: y c= J by A4, ZFMISC_1: 74;

          hence I c= J by A8;

          thus J is non empty by A8, A9;

          let A,B be Subset of L;

          assume

           A10: A in ZI & B in ZI;

          then (A,B) are_c=-comparable by A6, ORDINAL1:def 8;

          then A c= B or B c= A;

          then (A \/ B) = A or (A \/ B) = B by XBOOLE_1: 12;

          hence ex C be Subset of L st C in ZI & (A \/ B) c= C by A10;

        end;

        now

          let A be Subset of L;

          assume A in ZI;

          then A in X by A5;

          then ex P be Ideal of L st A = P & I c= P & P misses F;

          hence A is directed;

        end;

        then

        reconsider J as Ideal of L by A7, WAYBEL_0: 46;

        now

          let x be object;

          assume x in J;

          then

          consider A be 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;

        end;

        then J misses F by XBOOLE_0: 3;

        hence ( union Z) in X by A7;

      end;

      I in X by A1;

      then

      consider Y be set such that

       A13: Y in X and

       A14: for Z be set st Z in X & Z <> Y holds not Y c= Z by A3, ORDERS_1: 67;

      consider P be Ideal of L such that

       A15: P = Y and

       A16: I c= P and

       A17: P misses F by A13;

      take P;

      hereby

        let x,y be Element of L;

        assume that

         A18: (x "/\" y) in P and

         A19: not x in P and

         A20: not y in P;

        set Py = ( downarrow ( finsups (P \/ {y})));



         A21: (P \/ {y}) c= Py by WAYBEL_0: 61;



         A22: P c= (P \/ {y}) by XBOOLE_1: 7;

        then P c= Py by A21;

        then

         A23: I c= Py by A16;

        y in {y} by TARSKI:def 1;

        then y in (P \/ {y}) by XBOOLE_0:def 3;

        then

         A24: y in Py by A21;

        now

          assume Py misses F;

          then Py in X by A23;

          hence contradiction by A14, A15, A20, A21, A22, A24, XBOOLE_1: 1;

        end;

        then

        consider v be object such that

         A25: v in Py and

         A26: v in F by XBOOLE_0: 3;

        set Px = ( downarrow ( finsups (P \/ {x})));



         A27: (P \/ {x}) c= Px by WAYBEL_0: 61;



         A28: P c= (P \/ {x}) by XBOOLE_1: 7;

        then P c= Px by A27;

        then

         A29: I c= Px by A16;

        x in {x} by TARSKI:def 1;

        then x in (P \/ {x}) by XBOOLE_0:def 3;

        then

         A30: x in Px by A27;

        now

          assume Px misses F;

          then Px in X by A29;

          hence contradiction by A14, A15, A19, A27, A28, A30, XBOOLE_1: 1;

        end;

        then

        consider u be object such that

         A31: u in Px and

         A32: u in F by XBOOLE_0: 3;

        reconsider u, v as Element of L by A31, A25;

        consider u9 be Element of L such that

         A33: u9 in P and

         A34: u <= (u9 "\/" ( sup {x})) by A31, Lm2;

        consider v9 be 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 & (w "\/" x) >= (u9 "\/" x) by YELLOW_0: 22, YELLOW_0: 39;

        then (w "\/" x) >= u by A34, ORDERS_2: 3;

        then

         A37: (w "\/" x) in F by A32, WAYBEL_0:def 20;

        (w "\/" y) = (u9 "\/" (v9 "\/" y)) by LATTICE3: 14;

        then ( sup {y}) = y & (w "\/" y) >= (v9 "\/" y) by YELLOW_0: 22, YELLOW_0: 39;

        then (w "\/" y) >= v by A36, ORDERS_2: 3;

        then (w "\/" y) in F by A26, WAYBEL_0:def 20;

        then ((w "\/" x) "/\" (w "\/" y)) in F by A37, WAYBEL_0: 41;

        then

         A38: (w "\/" (x "/\" y)) in F by WAYBEL_1: 5;

        w in P by A33, A35, WAYBEL_0: 40;

        then (w "\/" (x "/\" y)) in P by A18, WAYBEL_0: 40;

        hence contradiction by A17, A38, XBOOLE_0: 3;

      end;

      thus thesis by A16, A17;

    end;

    theorem :: WAYBEL_7:24



     Th24: for L be distributive LATTICE, I be Ideal of L, x be Element of L st not x in I holds ex P be Ideal of L st P is prime & I c= P & not x in P

    proof

      let L be distributive LATTICE, I be Ideal of L, x be Element of L such that

       A1: not x in I;

      now

        let a be object;

        assume that

         A2: a in I and

         A3: a in ( uparrow x);

        reconsider a as Element of L by A2;

        a >= x by A3, WAYBEL_0: 18;

        hence contradiction by A1, A2, WAYBEL_0:def 19;

      end;

      then I misses ( uparrow x) by XBOOLE_0: 3;

      then

      consider P be Ideal of L such that

       A4: P is prime & I c= P and

       A5: P misses ( uparrow x) by Th23;

      take P;

      thus P is prime & I c= P by A4;

      assume x in P;

      then not x in ( uparrow x) by A5, XBOOLE_0: 3;

      then not x <= x by WAYBEL_0: 18;

      hence thesis;

    end;

    theorem :: WAYBEL_7:25



     Th25: for L be distributive LATTICE, I be Ideal of L, F be Filter of L st I misses F holds ex P be Filter of L st P is prime & F c= P & I misses P

    proof

      let L be distributive LATTICE, I be Ideal of L, F be Filter of L such that

       A1: I misses F;

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

      thus thesis by A2, Th17;

    end;

    theorem :: WAYBEL_7:26



     Th26: for L be non trivial Boolean LATTICE, F be proper Filter of L holds ex G be Filter of L st F c= G & G is ultra

    proof

      let L be non trivial Boolean LATTICE;

      let F be proper Filter of L;

      ( downarrow ( Bottom L)) = {( Bottom L)} by WAYBEL_4: 23;

      then

      reconsider I = {( Bottom L)} as Ideal of L;

      now

        let a be object;

        assume a in I;

        then a = ( Bottom L) by TARSKI:def 1;

        hence not a in F by Th4;

      end;

      then I misses F by XBOOLE_0: 3;

      then

      consider G be Filter of L such that

       A1: G is prime & F c= G and

       A2: I misses G by Th25;

      take G;

      now

        assume ( Bottom L) in G;

        then not ( Bottom L) in I by A2, XBOOLE_0: 3;

        hence contradiction by TARSKI:def 1;

      end;

      then G is proper;

      hence thesis by A1, Th22;

    end;

    begin

    definition

      let T be TopSpace;

      let F be set, x be object;

      :: WAYBEL_7:def4

      pred x is_a_cluster_point_of F,T means for A be Subset of T st A is open & x in A holds for B be set st B in F holds A meets B;

      :: WAYBEL_7:def5

      pred x is_a_convergence_point_of F,T means for A be Subset of T st A is open & x in A holds A in F;

    end

    registration

      let X be non empty set;

      cluster ultra for Filter of ( BoolePoset X);

      existence

      proof

        set F = the proper Filter of ( BoolePoset X);

        ex G be Filter of ( BoolePoset X) st F c= G & G is ultra by Th26;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_7:27



     Th27: for T be non empty TopSpace holds for F be ultra Filter of ( BoolePoset the carrier of T) holds for p be 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;

      set L = ( BoolePoset the carrier of T);

      let F be ultra Filter of L;

      let p be set;

      thus p is_a_cluster_point_of (F,T) implies p is_a_convergence_point_of (F,T)

      proof

        assume

         A1: for A be Subset of T st A is open & p in A holds for B be set st B in F holds A meets B;

        let A be Subset of T;

        assume that

         A2: A is open & p in A and

         A3: not A in F;

        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;

      end;

      assume

       A4: for A be Subset of T st A is open & p in A holds A in F;

      let A be Subset of T;

      assume A is open & p in A;

      then

       A5: A in F by A4;

      ( Bottom L) = {} by YELLOW_1: 18;

      then

       A6: not {} in F by Th4;

      let B be set;

      assume

       A7: B in F;

      then

      reconsider a = A, b = B as Element of L by A5;

      (a "/\" b) = (A /\ B) by YELLOW_1: 17;

      then (A /\ B) in F by A5, A7, WAYBEL_0: 41;

      hence thesis by A6;

    end;

    theorem :: WAYBEL_7:28



     Th28: for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st x << y holds for F be proper Filter of ( BoolePoset the carrier of T) st x in F holds ex p be Element of T st p in y & p is_a_cluster_point_of (F,T)

    proof

      defpred P[ object, object] means ex A,B be set st A = $1 & B = $2 & A misses B;

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      set B = ( BoolePoset the carrier of T);

      let x,y be Element of L such that

       A1: x << y;

      B = ( InclPoset ( bool the carrier of T)) by YELLOW_1: 4;

      then

       A2: B = RelStr (# ( bool the carrier of T), ( RelIncl ( bool the carrier of T)) #) by YELLOW_1:def 1;

      x in the carrier of L & L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      then

      reconsider x9 = x as Element of B by A2;

      let F be proper Filter of B such that

       A3: x in F and

       A4: for x be Element of T st x in y holds not x is_a_cluster_point_of (F,T);

      set V = { A where A be Subset of T : A is open & A meets y & ex B be set st B in F & A misses B };

      V c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in V;

        then ex C be Subset of T st a = C & C is open & C meets y & ex B be set st B in F & C misses B;

        hence thesis;

      end;

      then

      reconsider V as Subset-Family of T;

      reconsider V as Subset-Family of T;



       A5: y c= ( union V)

      proof

        let x be object;

        assume

         A6: x in y;

        L = 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 be Subset of T such that

         A7: A is open and

         A8: x in A and

         A9: ex B be set st B in F & A misses B;

        A meets y by A6, A8, XBOOLE_0: 3;

        then A in V by A7, A9;

        hence thesis by A8, TARSKI:def 4;

      end;

      V is open

      proof

        let a be Subset of T;

        assume a in V;

        then ex C be Subset of T st a = C & C is open & C meets y & ex B be set st B in F & C misses B;

        hence thesis;

      end;

      then

      consider W be finite Subset of V such that

       A10: x c= ( union W) by A1, A5, WAYBEL_3: 34;

       A11:

      now

        let A be object;

        assume A in W;

        then A in V;

        then ex C be Subset of T st A = C & C is open & C meets y & ex B be set st B in F & C misses B;

        hence ex B be object st B in F & P[A, B];

      end;

      consider f be Function such that

       A12: ( dom f) = W & ( rng f) c= F & for A be object st A in W holds P[A, (f . A)] from FUNCT_1:sch 6( A11);

      ( rng f) is finite by A12, FINSET_1: 8;

      then

      consider z be 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 B) by Th4;

      then (x9 "/\" z) <> {} by YELLOW_1: 18;

      then

       A15: a in (x9 "/\" z);



       A16: (x9 "/\" z) c= (x9 /\ z) by YELLOW_1: 17;

      then a in x by A15, XBOOLE_0:def 4;

      then

      consider A be set such that

       A17: a in A and

       A18: A in W by A10, TARSKI:def 4;



       A19: a 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 B;

      z <= b by A14, A20, LATTICE3:def 8;

      then

       A21: z c= b by YELLOW_1: 2;

       P[A, (f . A)] by A12, A18;

      then A misses b;

      hence contradiction by A19, A17, A21, XBOOLE_0: 3;

    end;

    theorem :: WAYBEL_7:29

    for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st x << y holds for F be ultra Filter of ( BoolePoset the carrier of T) st x in F holds ex p be Element of T st p in y & p is_a_convergence_point_of (F,T)

    proof

      let T be non empty TopSpace;

      let x,y be Element of ( InclPoset the topology of T) such that

       A1: x << y;

      let F be ultra Filter of ( BoolePoset the carrier of T);

      assume x in F;

      then

      consider p be Element of T such that

       A2: p in y & p is_a_cluster_point_of (F,T) by A1, Th28;

      take p;

      thus thesis by A2, Th27;

    end;

    theorem :: WAYBEL_7:30



     Th30: for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st x c= y & for F be ultra Filter of ( BoolePoset the carrier of T) st x in F holds ex p be 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;

      set B = ( BoolePoset the carrier of T);

      let x,y be Element of ( InclPoset the topology of T) such that

       A1: x c= y and

       A2: for F be ultra Filter of B st x in F holds ex p be Element of T st p in y & p is_a_convergence_point_of (F,T);

      ( 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 as Subset of T;

      assume not x << y;

      then

      consider F be Subset-Family of T such that

       A3: F is open and

       A4: y c= ( union F) and

       A5: not ex G be finite Subset of F st x c= ( union G) by WAYBEL_3: 35;

      set xF = { (x \ z) where z be Subset of T : z in F };

      set z = the Element of F;

       A6:

      now

        assume

         A7: F = {} ;

        then y = {} by A4, ZFMISC_1: 2;

        then x = y by A1;

        hence contradiction by A4, A5, A7;

      end;

      then

       A8: z in F;

      B = ( InclPoset ( bool the carrier of T)) by YELLOW_1: 4;

      then

       A9: B = RelStr (# ( bool the carrier of T), ( RelIncl ( bool the carrier of T)) #) by YELLOW_1:def 1;

      xF c= the carrier of B

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume a in xF;

        then ex z be Subset of T st a = (x \ z) & z in F;

        then aa c= X;

        then aa c= the carrier of T by XBOOLE_1: 1;

        hence thesis by A9;

      end;

      then

      reconsider xF as Subset of B;

      set FF = ( uparrow ( fininfs xF));

      now

        defpred P[ object, object] means ex A be set st A = $2 & $1 = (x \ A);

        assume ( Bottom B) in FF;

        then

        consider a be Element of B such that

         A10: a <= ( Bottom B) and

         A11: a in ( fininfs xF) by WAYBEL_0:def 16;

        consider s be finite Subset of xF such that

         A12: a = ( "/\" (s,B)) and ex_inf_of (s,B) by A11;

        reconsider t = s as Subset of B by XBOOLE_1: 1;

         A13:

        now

          let v be object;

          assume v in s;

          then v in xF;

          then ex z be Subset of T st v = (x \ z) & z in F;

          hence ex z be object st z in F & P[v, z];

        end;

        consider f be Function such that

         A14: ( dom f) = s & ( rng f) c= F & for v be object st v in s holds P[v, (f . v)] from FUNCT_1:sch 6( A13);

        reconsider G = ( rng f) as finite Subset of F by A14, FINSET_1: 8;

        ( Bottom B) = {} by YELLOW_1: 18;

        then

         A15: a c= {} by A10, YELLOW_1: 2;

         A16:

        now

          assume s = {} ;

          then a = ( Top B) by A12;

          hence contradiction by A15, YELLOW_1: 19;

        end;

        then

         A17: a = ( meet t) by A12, YELLOW_1: 20;

        x c= ( union G)

        proof

          let c be object;

          assume that

           A18: c in x and

           A19: not c in ( union G);

          now

            let v be set;

            assume

             A20: v in s;

            then (f . v) in ( rng f) by A14, FUNCT_1:def 3;

            then

             A21: not c in (f . v) by A19, TARSKI:def 4;

             P[v, (f . v)] by A14, A20;

            then v = (x \ (f . v));

            hence c in v by A18, A21, XBOOLE_0:def 5;

          end;

          hence contradiction by A15, A16, A17, SETFAM_1:def 1;

        end;

        hence contradiction by A5;

      end;

      then FF is proper;

      then

      consider GG be Filter of B such that

       A22: FF c= GG and

       A23: GG is ultra by Th26;

      reconsider z as Subset of T by A8;



       A24: xF c= FF by WAYBEL_0: 62;

      (x \ z) in xF by A6;

      then

       A25: (x \ z) in FF by A24;

      (x \ z) c= X;

      then x in GG by A22, A25, Th7;

      then

      consider p be Element of T such that

       A26: p in y and

       A27: p is_a_convergence_point_of (GG,T) by A2, A23;

      consider W be set such that

       A28: p in W and

       A29: W in F by A4, A26, TARSKI:def 4;

      reconsider W as Subset of T by A29;

      W is open by A3, A29;

      then

       A30: W in GG by A27, A28;



       A31: xF c= FF by WAYBEL_0: 62;

      (x \ W) in xF by A29;

      then (x \ W) in FF by A31;

      then W misses (x \ W) & (W /\ (x \ W)) in GG by A22, A30, Th9, XBOOLE_1: 79;

      then {} in GG;

      then ( Bottom B) in GG by YELLOW_1: 18;

      hence thesis by A23, Th4;

    end;

    ::$Notion-Name

    theorem :: WAYBEL_7:31

    for T be non empty TopSpace holds for B be prebasis of T holds for x,y be Element of ( InclPoset the topology of T) st x c= y holds x << y iff for F be Subset of B st y c= ( union F) holds ex G be finite Subset of F st x c= ( union G)

    proof

      let T be non empty TopSpace, B be prebasis of T;

      consider BB be 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 L such that

       A2: x c= y;



       A3: B c= the topology of T by TOPS_2: 64;

      hereby

        assume

         A4: x << y;

        let F be Subset of B such that

         A5: y c= ( union F);

        reconsider FF = F as Subset-Family of T by XBOOLE_1: 1;

        FF is open

        proof

          let a be Subset of T;

          assume a in FF;

          then a in B;

          hence a in the topology of T by A3;

        end;

        hence ex G be finite Subset of F st x c= ( union G) by A4, A5, WAYBEL_3: 34;

      end;

      BT = ( InclPoset ( bool the carrier of T)) by YELLOW_1: 4;

      then

       A6: BT = RelStr (# ( bool the carrier of T), ( RelIncl ( bool the carrier of T)) #) by YELLOW_1:def 1;

      L = 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 be Subset of B st y c= ( union F) holds ex G be finite Subset of F st x c= ( union G);



       A8: the topology of T c= ( UniCl BB) by CANTOR_1:def 2;

      now

        deffunc F( set) = (x \ $1);

        let F be ultra Filter of ( BoolePoset the carrier of T) such that

         A9: x in F and

         A10: not ex p be Element of T st p in y & p is_a_convergence_point_of (F,T);

        defpred P[ object, object] means ex A be set st A = $2 & $1 in A & not $2 in F;

         A11:

        now

          let p be object;

          assume

           A12: p in y;

          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 be Subset of T such that

           A13: A is open and

           A14: q in A and

           A15: not A in F;

          A in the topology of T by A13;

          then

          consider AY be Subset-Family of T such that

           A16: AY c= BB and

           A17: A = ( union AY) by A8, CANTOR_1:def 1;

          consider ay be set such that

           A18: q in ay and

           A19: ay in AY by A14, A17, TARSKI:def 4;

          reconsider ay as Subset of T by A19;

          ay in BB by A16, A19;

          then

          consider BY be 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 not BY is Subset of F by A21, A22, Th11;

          then

          consider r be object such that

           A23: r in BY & not r in F by TARSKI:def 3;

          reconsider A = r as set by TARSKI: 1;

          take r;

          thus r in B by A20, A23;

          thus P[p, r]

          proof

            take A;

            thus A = r & p in A & not r in F by A18, A22, A23, SETFAM_1: 43;

          end;

        end;

        consider f be Function such that

         A24: ( dom f) = y & ( rng f) c= B and

         A25: for p be object st p in y holds P[p, (f . p)] from FUNCT_1:sch 6( A11);

        reconsider FF = ( rng f) as Subset of B by A24;

        y c= ( union FF)

        proof

          let p be object;

          assume

           A26: p in y;

          then

          consider A be set such that

           A27: A = (f . p) & p in A & not (f . p) in F by A25;

          (f . p) in FF & p in (f . p) by A24, FUNCT_1:def 3, A27, A26;

          hence thesis by TARSKI:def 4;

        end;

        then

        consider G be finite Subset of FF such that

         A28: x c= ( union G) by A7;

        set gg = the Element of G;

        consider g be Function such that

         A29: ( dom g) = G & for z be set st z in G holds (g . z) = F(z) from FUNCT_1:sch 5;



         A30: ( rng g) c= F

        proof

          let a be object;



           A31: F is prime by Th22;

          assume a in ( rng g);

          then

          consider b be object such that

           A32: b in G and

           A33: a = (g . b) by A29, FUNCT_1:def 3;

          b in FF by A32;

          then b in B;

          then

          reconsider b as Subset of T;

          consider p be object such that

           A34: p in y & b = (f . p) by A24, A32, FUNCT_1:def 3;

           P[p, (f . p)] by A25, A34;

          then not b in F by A34;

          then

           A35: (the carrier of T \ b) in F by A31, Th21;

          a = (x \ b) by A29, A32, A33

          .= (X /\ (b ` )) by SUBSET_1: 13

          .= (x /\ (the carrier of T \ b));

          hence thesis by A9, A35, Th9;

        end;

        then

        reconsider GG = ( rng g) as finite Subset-Family of T by A6, A29, FINSET_1: 8, XBOOLE_1: 1;

        x <> ( Bottom ( BoolePoset the carrier of T)) by A9, Th4;

        then x <> {} by YELLOW_1: 18;

        then

         A36: G <> {} by A28, ZFMISC_1: 2;

        now

          let a be object;

          assume

           A37: a in ( Intersect GG);

          now

            let z be set;

            assume z in G;

            then (g . z) in GG & (g . z) = (x \ z) by A29, FUNCT_1:def 3;

            then a in (x \ z) by A37, SETFAM_1: 43;

            hence not a in z by XBOOLE_0:def 5;

          end;

          then not ex z be set st a in z & z in G;

          then

           A38: not a in x by A28, TARSKI:def 4;

          (g . gg) in GG & (g . gg) = (x \ gg) by A36, A29, FUNCT_1:def 3;

          then a in (x \ gg) by A37, SETFAM_1: 43;

          hence contradiction by A38;

        end;

        then

         A39: ( Intersect GG) = {} by XBOOLE_0:def 1;

        ( Intersect GG) in F by A30, Th11;

        then ( Bottom ( BoolePoset the carrier of T)) in F by A39, YELLOW_1: 18;

        hence contradiction by Th4;

      end;

      hence thesis by A2, Th30;

    end;

    theorem :: WAYBEL_7:32

    for L be distributive complete LATTICE holds for x,y be Element of L holds x << y iff for P be prime Ideal of L st y <= ( sup P) holds x in P

    proof

      let L be distributive complete LATTICE;

      let x,y be Element of L;

      thus x << y implies for P be prime Ideal of L st y <= ( sup P) holds x in P by WAYBEL_3: 20;

      assume

       A1: for P be prime Ideal of L st y <= ( sup P) holds x in P;

      now

        let I be Ideal of L;

        assume that

         A2: y <= ( sup I) and

         A3: not x in I;

        consider P be 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;

      end;

      hence thesis by WAYBEL_3: 21;

    end;

    theorem :: WAYBEL_7:33



     Th33: for L be LATTICE, p be Element of L st p is prime holds ( downarrow p) is prime

    proof

      let L be LATTICE, p be Element of L such that

       A1: for x,y be Element of L st (x "/\" y) <= p holds x <= p or y <= p;

      let x,y be Element of L;

      assume (x "/\" y) in ( downarrow p);

      then (x "/\" y) <= p by WAYBEL_0: 17;

      then x <= p or y <= p by A1;

      hence thesis by WAYBEL_0: 17;

    end;

    begin

    definition

      let L be LATTICE;

      let p be Element of L;

      :: WAYBEL_7:def6

      attr p is pseudoprime means ex P be prime Ideal of L st p = ( sup P);

    end

    theorem :: WAYBEL_7:34



     Th34: for L be LATTICE holds for p be Element of L st p is prime holds p is pseudoprime

    proof

      let L be LATTICE, p be Element of L;

      assume p is prime;

      then

       A1: ( downarrow p) is prime by Th33;

      p = ( sup ( downarrow p)) by WAYBEL_0: 34;

      hence ex P be prime Ideal of L st p = ( sup P) by A1;

    end;

    theorem :: WAYBEL_7:35



     Th35: for L be continuous LATTICE holds for p be Element of L st p is pseudoprime holds for A be finite non empty Subset of L st ( inf A) << p holds ex a be Element of L st a in A & a <= p

    proof

      let L be continuous LATTICE;

      let p be Element of L;

      given P be prime Ideal of L such that

       A1: p = ( sup P);

      let A be finite non empty Subset of L;

      assume ( inf A) << p;

      then

       A2: ( inf A) in ( waybelow p);

      ( waybelow p) c= P by A1, WAYBEL_5: 1;

      then

      consider a be Element of L such that

       A3: a in A & a in P by A2, Th12;

      take a;

       ex_sup_of (P,L) by WAYBEL_0: 75;

      then P is_<=_than p by A1, YELLOW_0: 30;

      hence thesis by A3, LATTICE3:def 9;

    end;

    theorem :: WAYBEL_7:36

    for L be continuous LATTICE holds for p be Element of L st (p <> ( Top L) or not ( Top L) is compact) & for A be finite non empty Subset of L st ( inf A) << p holds ex a be Element of L st a in A & a <= p holds ( uparrow ( fininfs (( downarrow p) ` ))) misses ( waybelow p)

    proof

      let L be continuous LATTICE, p be Element of L such that

       A1: p <> ( Top L) or not ( Top L) is compact and

       A2: for A be finite non empty Subset of L st ( inf A) << p holds ex a be Element of L st a in A & a <= p;

      now

        let x be object;

        assume

         A3: x in ( uparrow ( fininfs (( downarrow p) ` )));

        then

        reconsider a = x as Element of L;

        consider b be 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);

        then

         A6: a << p by WAYBEL_3: 7;

        then

         A7: b << p by A4, WAYBEL_3: 2;

        consider Y be finite Subset of (( downarrow p) ` ) such that

         A8: b = ( "/\" (Y,L)) and ex_inf_of (Y,L) by A5;

        reconsider Y as finite Subset of L by XBOOLE_1: 1;

        per cases ;

          suppose Y <> {} ;

          then

          consider c be 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;

        end;

          suppose

           A11: Y = {} ;

          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;

        end;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: WAYBEL_7:37

    for L be continuous LATTICE st ( Top L) is compact holds (for A be finite non empty Subset of L st ( inf A) << ( Top L) holds ex a be 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 such that

       A1: ( Top L) << ( Top L);

       A2:

      now

        take x = ( Top L);

        thus x in ( uparrow ( fininfs (( downarrow ( Top L)) ` ))) by WAYBEL_4: 22;

        thus x in ( waybelow ( Top L)) by A1;

      end;

      hereby

        let A be finite non empty Subset of L such that ( inf A) << ( Top L);

        set a = the Element of A;

        reconsider a as Element of L;

        take a;

        thus a in A & a <= ( Top L) by YELLOW_0: 45;

      end;

      thus thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: WAYBEL_7:38

    for L be continuous LATTICE holds for p be Element of L st ( uparrow ( fininfs (( downarrow p) ` ))) misses ( waybelow p) holds for A be finite non empty Subset of L st ( inf A) << p holds ex a be Element of L st a in A & a <= p

    proof

      let L be continuous LATTICE, p be Element of L such that

       A1: ( uparrow ( fininfs (( downarrow p) ` ))) misses ( waybelow p);

      let A be finite non empty Subset of L;

      assume ( inf 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) ` );

      then

      consider a be object such that

       A2: a in A and

       A3: not a in (( downarrow p) ` );

      reconsider a as Element of L by A2;

      take a;

      a in ( downarrow p) by A3, SUBSET_1: 29;

      hence thesis by A2, WAYBEL_0: 17;

    end;

    theorem :: WAYBEL_7:39

    for L be distributive continuous LATTICE holds for p be Element of L st ( uparrow ( fininfs (( downarrow p) ` ))) misses ( waybelow p) holds p is pseudoprime

    proof

      let L be distributive continuous LATTICE;

      let p be Element of L;

      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= F by WAYBEL_0: 62;

      then

       A2: (F ` ) c= ((( downarrow p) ` ) ` ) by SUBSET_1: 12;

      assume F misses I;

      then

      consider P be Ideal of L such that

       A3: P is prime and

       A4: I c= P and

       A5: P misses F by Th23;

      reconsider P as prime Ideal of L by A3;



       A6: ex_sup_of (P,L) by WAYBEL_0: 75;

       ex_sup_of (I,L) & p = ( sup I) by WAYBEL_0: 75, WAYBEL_3:def 5;

      then

       A7: ( sup P) >= p by A4, A6, YELLOW_0: 34;

      take P;

      P c= (F ` ) by A5, SUBSET_1: 23;

      then ( sup P) <= p by A6, A2, A1, XBOOLE_1: 1, YELLOW_0: 34;

      hence thesis by A7, ORDERS_2: 2;

    end;

    definition

      let L be non empty RelStr;

      let R be Relation of the carrier of L;

      :: WAYBEL_7:def7

      attr R is multiplicative means for a,x,y be Element of L st [a, x] in R & [a, y] in R holds [a, (x "/\" y)] in R;

    end

    registration

      let L be lower-bounded sup-Semilattice;

      let R be auxiliary Relation of L;

      let x be Element of L;

      cluster (R -above x) -> upper;

      coherence

      proof

        let y,z be Element of L;

        assume that

         A1: y in (R -above x) and

         A2: y <= z;

        x <= x & [x, y] in R by A1, WAYBEL_4: 14;

        then [x, z] in R by A2, WAYBEL_4:def 4;

        hence thesis by WAYBEL_4: 14;

      end;

    end

    theorem :: WAYBEL_7:40

    for L be lower-bounded LATTICE, R be auxiliary Relation of L holds R is multiplicative iff for x be Element of L holds (R -above x) is filtered

    proof

      let L be lower-bounded LATTICE, R be auxiliary Relation of L;

      hereby

        assume

         A1: R is multiplicative;

        let x be Element of L;

        thus (R -above x) is filtered

        proof

          let y,z be Element of L;

          assume y in (R -above x) & z in (R -above x);

          then [x, y] in R & [x, z] in R by WAYBEL_4: 14;

          then [x, (y "/\" z)] in R by A1;

          then

           A2: (y "/\" z) in (R -above x) by WAYBEL_4: 14;

          y >= (y "/\" z) & z >= (y "/\" z) by YELLOW_0: 23;

          hence thesis by A2;

        end;

      end;

      assume

       A3: for x be Element of L holds (R -above x) is filtered;

      let a,x,y be Element of L;

      assume [a, x] in R & [a, 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;

    end;

    theorem :: WAYBEL_7:41



     Th41: for L be lower-bounded LATTICE, R be auxiliary Relation of L holds R is multiplicative iff for a,b,x,y be 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, R be auxiliary Relation of L;

      hereby

        assume

         A1: R is multiplicative;

        let a,b,x,y be Element of L;

        assume that

         A2: [a, x] in R and

         A3: [b, 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;

      end;

      assume

       A5: for a,b,x,y be Element of L st [a, x] in R & [b, y] in R holds [(a "/\" b), (x "/\" y)] in R;

      let a be Element of L;

      (a "/\" a) = a by YELLOW_0: 25;

      hence thesis by A5;

    end;

    theorem :: WAYBEL_7:42

    for L be lower-bounded LATTICE, R be auxiliary Relation of L holds R is multiplicative iff for S be full SubRelStr of [:L, L:] st the carrier of S = R holds S is meet-inheriting

    proof

      let L be lower-bounded LATTICE, R be auxiliary Relation of L;

      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

        assume

         A2: R is multiplicative;

        let S be full SubRelStr of [:L, L:] such that

         A3: the carrier of S = R;

        thus S is meet-inheriting

        proof

          let x,y be Element of [:L, L:];

          assume

           A4: x in the carrier of S & y 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 thesis by A2, A3, A4, A5, Th41;

        end;

      end;

      assume for S be full SubRelStr of [:L, L:] st the carrier of S = R holds S is meet-inheriting;

      then

       A6: ( subrelstr X) is meet-inheriting by A1;

      let a,x,y be Element of L;



       A7: ex_inf_of ( { [a, x], [a, y]}, [:L, L:]) by YELLOW_0: 21;

      assume [a, x] in R & [a, y] in R;

      then ( inf { [a, x], [a, y]}) in R by A1, A6, A7;

      then

       A8: ( [a, x] "/\" [a, y]) in R by YELLOW_0: 40;

      set ax = [a, x], ay = [a, y];

      ( [a, x] "/\" [a, y]) = ( inf {ax, ay}) by YELLOW_0: 40

      .= [( inf ( proj1 {ax, ay})), ( inf ( proj2 {ax, ay}))] by A7, YELLOW_3: 47

      .= [( inf {a, a}), ( inf ( proj2 {ax, ay}))] 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;

    end;

    theorem :: WAYBEL_7:43

    for L be lower-bounded LATTICE, R be auxiliary Relation of L holds R is multiplicative iff (R -below ) is meet-preserving

    proof

      let L be lower-bounded LATTICE, R be auxiliary Relation of L;

      hereby

        assume

         A1: R is multiplicative;

        thus (R -below ) is meet-preserving

        proof

          let x,y be Element of L;



           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

              let a be object;

              assume a in (R -below (x "/\" y));

              then a in { z where z be Element of L : [z, (x "/\" y)] in R } by WAYBEL_4:def 10;

              then

              consider z be 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;

            end;

            let a be object;

            assume

             A8: a in ((R -below x) /\ (R -below 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;

            hence thesis by WAYBEL_4: 13;

          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 thesis by YELLOW_3: 8;

        end;

      end;

      assume

       A10: for x,y be Element of L holds (R -below ) preserves_inf_of {x, y};

      let a,x,y be Element of L;

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

      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 thesis by WAYBEL_4: 13;

    end;

     Lm3:

    now

      let L be continuous lower-bounded LATTICE, p be Element of L such that

       A1: (L -waybelow ) is multiplicative and

       A2: for a,b be Element of L st (a "/\" b) << p holds a <= p or b <= p and

       A3: not p is prime;

      consider x,y be Element of L such that

       A4: (x "/\" y) <= p and

       A5: not x <= p and

       A6: not y <= p by A3;



       A7: for a be Element of L holds ( waybelow a) is non empty directed;

      then

      consider u be Element of L such that

       A8: u << x and

       A9: not u <= p by A5, WAYBEL_3: 24;

      consider v be 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;

    end;

    theorem :: WAYBEL_7:44



     Th44: for L be continuous lower-bounded LATTICE st (L -waybelow ) is multiplicative holds for p be Element of L holds p is pseudoprime iff for a,b be Element of L st (a "/\" b) << p holds a <= p or b <= p

    proof

      let L be continuous lower-bounded LATTICE such that

       A1: (L -waybelow ) is multiplicative;

      let p be Element of L;

      hereby

        assume

         A2: p is pseudoprime;

        let a,b be Element of L;

        assume (a "/\" b) << p;

        then ( inf {a, b}) << p by YELLOW_0: 40;

        then ex c be Element of L st c in {a, b} & c <= p by A2, Th35;

        hence a <= p or b <= p by TARSKI:def 2;

      end;

      assume for a,b be Element of L st (a "/\" b) << p holds a <= p or b <= p;

      hence thesis by A1, Lm3, Th34;

    end;

    theorem :: WAYBEL_7:45

    for L be continuous lower-bounded LATTICE st (L -waybelow ) is multiplicative holds for p be Element of L st p is pseudoprime holds p is prime

    proof

      let L be continuous lower-bounded LATTICE such that

       A1: (L -waybelow ) is multiplicative;

      let p be Element of L;

      assume p is pseudoprime;

      then for a,b be Element of L st (a "/\" b) << p holds a <= p or b <= p by A1, Th44;

      hence thesis by A1, Lm3;

    end;

    theorem :: WAYBEL_7:46

    for L be distributive continuous lower-bounded LATTICE st for p be Element of L st p is pseudoprime holds p is prime holds (L -waybelow ) is multiplicative

    proof

      let L be distributive continuous lower-bounded LATTICE such that

       A1: for p be Element of L st p is pseudoprime holds p is prime;

      given a,x,y be 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 );

      now

        let z be object;

        assume that

         A4: z in ( waybelow (x "/\" y)) and

         A5: z in ( uparrow a);

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

      end;

      then ( waybelow (x "/\" y)) misses ( uparrow a) by XBOOLE_0: 3;

      then

      consider P be 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);

      p is pseudoprime by A6;

      then

       A9: 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) <= p by A7, A11, YELLOW_0: 34;

      then x <= p & a << x or y <= p & a << y by A2, A9, WAYBEL_4:def 1;

      then a in P by WAYBEL_3: 20;

      hence thesis by A8, A10, XBOOLE_0: 3;

    end;