waybel14.miz



    begin

    theorem :: WAYBEL14:1

    

     Th1: for X be set, F be finite Subset-Family of X holds ex G be finite Subset-Family of X st G c= F & ( union G) = ( union F) & for g be Subset of X st g in G holds not g c= ( union (G \ {g}))

    proof

      let X be set;

      defpred P[ Nat] means for F be finite Subset-Family of X st ( card F) = $1 holds ex G be finite Subset-Family of X st G c= F & ( union G) = ( union F) & for g be Subset of X st g in G holds not g c= ( union (G \ {g}));

       A1:

      now

        let n be Nat;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let F be finite Subset-Family of X;

          assume

           A3: ( card F) = (n + 1);

          per cases ;

            suppose ex g be Subset of X st g in F & g c= ( union (F \ {g}));

            then

            consider g be Subset of X such that

             A4: g in F and

             A5: g c= ( union (F \ {g}));

            reconsider FF = (F \ {g}) as finite Subset-Family of X;

             {g} c= F by A4, ZFMISC_1: 31;

            then

             A6: F = (FF \/ {g}) by XBOOLE_1: 45;

            

             A7: ( union F) c= ( union FF)

            proof

              let x be object;

              assume x in ( union F);

              then

              consider X be set such that

               A8: x in X and

               A9: X in F by TARSKI:def 4;

              per cases by A6, A9, XBOOLE_0:def 3;

                suppose X in FF;

                then X c= ( union FF) by ZFMISC_1: 74;

                hence thesis by A8;

              end;

                suppose X in {g};

                then X = g by TARSKI:def 1;

                hence thesis by A5, A8;

              end;

            end;

            g in {g} by TARSKI:def 1;

            then not g in FF by XBOOLE_0:def 5;

            then ( card (FF \/ {g})) = (( card FF) + 1) by CARD_2: 41;

            then

            consider G be finite Subset-Family of X such that

             A10: G c= FF and

             A11: ( union G) = ( union FF) and

             A12: for g be Subset of X st g in G holds not g c= ( union (G \ {g})) by A2, A3, A6, XCMPLX_1: 2;

            take G;

            FF c= F by A6, XBOOLE_1: 7;

            hence G c= F by A10;

            ( union FF) c= ( union F) by A6, XBOOLE_1: 7, ZFMISC_1: 77;

            hence ( union G) = ( union F) by A11, A7;

            thus thesis by A12;

          end;

            suppose

             A13: not ex g be Subset of X st g in F & g c= ( union (F \ {g}));

            take G = F;

            thus G c= F;

            thus ( union G) = ( union F);

            thus thesis by A13;

          end;

        end;

      end;

      let F be finite Subset-Family of X;

      

       A14: ( card F) = ( card F);

      

       A15: P[ 0 ]

      proof

        let F be finite Subset-Family of X;

        assume

         A16: ( card F) = 0 ;

        take G = F;

        thus G c= F;

        thus ( union G) = ( union F);

        thus thesis by A16;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A15, A1);

      hence thesis by A14;

    end;

    

     Lm1: for S be 1-sorted, X,Y be Subset of S holds X c= (Y ` ) iff Y c= (X ` )

    proof

      let S be 1-sorted, X,Y be Subset of S;

      Y = ((Y ` ) ` );

      hence thesis by SUBSET_1: 12;

    end;

    theorem :: WAYBEL14:2

    

     Th2: for S be 1-sorted, X be Subset of S holds (X ` ) = the carrier of S iff X is empty

    proof

      let S be 1-sorted, X be Subset of S;

      hereby

        assume (X ` ) = the carrier of S;

        then X = (( [#] the carrier of S) ` );

        hence X is empty by XBOOLE_1: 37;

      end;

      assume X is empty;

      hence thesis;

    end;

    theorem :: WAYBEL14:3

    

     Th3: for R be antisymmetric with_infima transitive non empty RelStr, x,y be Element of R holds ( downarrow (x "/\" y)) = (( downarrow x) /\ ( downarrow y))

    proof

      let R be antisymmetric with_infima transitive non empty RelStr, x,y be Element of R;

      now

        let z be object;

        hereby

          assume

           A1: z in ( downarrow (x "/\" y));

          then

          reconsider z9 = z as Element of R;

          

           A2: z9 <= (x "/\" y) by A1, WAYBEL_0: 17;

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

          then z9 <= y by A2, YELLOW_0:def 2;

          then

           A3: z9 in ( downarrow y) by WAYBEL_0: 17;

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

          then z9 <= x by A2, YELLOW_0:def 2;

          then z9 in ( downarrow x) by WAYBEL_0: 17;

          hence z in (( downarrow x) /\ ( downarrow y)) by A3, XBOOLE_0:def 4;

        end;

        assume

         A4: z in (( downarrow x) /\ ( downarrow y));

        then

        reconsider z9 = z as Element of R;

        z in ( downarrow y) by A4, XBOOLE_0:def 4;

        then

         A5: z9 <= y by WAYBEL_0: 17;

        z in ( downarrow x) by A4, XBOOLE_0:def 4;

        then z9 <= x by WAYBEL_0: 17;

        then (x "/\" y) >= z9 by A5, YELLOW_0: 23;

        hence z in ( downarrow (x "/\" y)) by WAYBEL_0: 17;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:4

    for R be antisymmetric with_suprema transitive non empty RelStr, x,y be Element of R holds ( uparrow (x "\/" y)) = (( uparrow x) /\ ( uparrow y))

    proof

      let R be antisymmetric with_suprema transitive non empty RelStr, x,y be Element of R;

      now

        let z be object;

        hereby

          assume

           A1: z in ( uparrow (x "\/" y));

          then

          reconsider z9 = z as Element of R;

          

           A2: z9 >= (x "\/" y) by A1, WAYBEL_0: 18;

          (x "\/" y) >= y by YELLOW_0: 22;

          then z9 >= y by A2, YELLOW_0:def 2;

          then

           A3: z9 in ( uparrow y) by WAYBEL_0: 18;

          (x "\/" y) >= x by YELLOW_0: 22;

          then z9 >= x by A2, YELLOW_0:def 2;

          then z9 in ( uparrow x) by WAYBEL_0: 18;

          hence z in (( uparrow x) /\ ( uparrow y)) by A3, XBOOLE_0:def 4;

        end;

        assume

         A4: z in (( uparrow x) /\ ( uparrow y));

        then

        reconsider z9 = z as Element of R;

        z in ( uparrow y) by A4, XBOOLE_0:def 4;

        then

         A5: z9 >= y by WAYBEL_0: 18;

        z in ( uparrow x) by A4, XBOOLE_0:def 4;

        then z9 >= x by WAYBEL_0: 18;

        then (x "\/" y) <= z9 by A5, YELLOW_0: 22;

        hence z in ( uparrow (x "\/" y)) by WAYBEL_0: 18;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:5

    

     Th5: for L be complete antisymmetric non empty RelStr, X be lower Subset of L st ( sup X) in X holds X = ( downarrow ( sup X))

    proof

      let L be complete antisymmetric non empty RelStr, X be lower Subset of L such that

       A1: ( sup X) in X;

      X is_<=_than ( sup X) by YELLOW_0: 32;

      hence X c= ( downarrow ( sup X)) by YELLOW_2: 1;

      thus thesis by A1, WAYBEL11: 6;

    end;

    theorem :: WAYBEL14:6

    for L be complete antisymmetric non empty RelStr, X be upper Subset of L st ( inf X) in X holds X = ( uparrow ( inf X))

    proof

      let L be complete antisymmetric non empty RelStr, X be upper Subset of L such that

       A1: ( inf X) in X;

      X is_>=_than ( inf X) by YELLOW_0: 33;

      hence X c= ( uparrow ( inf X)) by YELLOW_2: 2;

      thus thesis by A1, WAYBEL11: 42;

    end;

    theorem :: WAYBEL14:7

    

     Th7: for R be non empty reflexive transitive RelStr, x,y be Element of R holds x << y iff ( uparrow y) c= ( wayabove x)

    proof

      let R be non empty reflexive transitive RelStr, x,y be Element of R;

      hereby

        assume

         A1: x << y;

        thus ( uparrow y) c= ( wayabove x)

        proof

          let z be object;

          assume

           A2: z in ( uparrow y);

          then

          reconsider z9 = z as Element of R;

          y <= z9 by A2, WAYBEL_0: 18;

          then x << z9 by A1, WAYBEL_3: 2;

          hence thesis;

        end;

      end;

      y <= y;

      then

       A3: y in ( uparrow y) by WAYBEL_0: 18;

      assume ( uparrow y) c= ( wayabove x);

      hence thesis by A3, WAYBEL_3: 8;

    end;

    theorem :: WAYBEL14:8

    for R be non empty reflexive transitive RelStr, x,y be Element of R holds x << y iff ( downarrow x) c= ( waybelow y)

    proof

      let R be non empty reflexive transitive RelStr, x,y be Element of R;

      hereby

        assume

         A1: x << y;

        thus ( downarrow x) c= ( waybelow y)

        proof

          let z be object;

          assume

           A2: z in ( downarrow x);

          then

          reconsider z9 = z as Element of R;

          z9 <= x by A2, WAYBEL_0: 17;

          then z9 << y by A1, WAYBEL_3: 2;

          hence thesis;

        end;

      end;

      x <= x;

      then

       A3: x in ( downarrow x) by WAYBEL_0: 17;

      assume ( downarrow x) c= ( waybelow y);

      hence thesis by A3, WAYBEL_3: 7;

    end;

    theorem :: WAYBEL14:9

    

     Th9: for R be complete reflexive antisymmetric non empty RelStr, x be Element of R holds ( sup ( waybelow x)) <= x & x <= ( inf ( wayabove x))

    proof

      let R be complete reflexive antisymmetric non empty RelStr, x be Element of R;

      x is_>=_than ( waybelow x) by WAYBEL_3: 9;

      hence ( sup ( waybelow x)) <= x by YELLOW_0: 32;

      x is_<=_than ( wayabove x) by WAYBEL_3: 10;

      hence thesis by YELLOW_0: 33;

    end;

    theorem :: WAYBEL14:10

    

     Th10: for L be lower-bounded antisymmetric non empty RelStr holds ( uparrow ( Bottom L)) = the carrier of L

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

      set uL = ( uparrow ( Bottom L)), cL = the carrier of L;

      for x be object holds x in uL iff x in cL by WAYBEL_0: 18, YELLOW_0: 44;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:11

    for L be upper-bounded antisymmetric non empty RelStr holds ( downarrow ( Top L)) = the carrier of L

    proof

      let L be upper-bounded antisymmetric non empty RelStr;

      set uL = ( downarrow ( Top L)), cL = the carrier of L;

      for x be object holds x in uL iff x in cL by WAYBEL_0: 17, YELLOW_0: 45;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:12

    

     Th12: for P be with_suprema Poset, x,y be Element of P holds (( wayabove x) "\/" ( wayabove y)) c= ( uparrow (x "\/" y))

    proof

      let R be with_suprema Poset, x,y be Element of R;

      ( {x} "\/" {y}) = {(x "\/" y)} & (( uparrow x) "\/" ( uparrow y)) c= ( uparrow (( uparrow x) "\/" ( uparrow y))) by WAYBEL_0: 16, YELLOW_4: 19;

      then

       A1: (( uparrow x) "\/" ( uparrow y)) c= ( uparrow (x "\/" y)) by YELLOW_4: 35;

      ( wayabove x) c= ( uparrow x) & ( wayabove y) c= ( uparrow y) by WAYBEL_3: 11;

      then (( wayabove x) "\/" ( wayabove y)) c= (( uparrow x) "\/" ( uparrow y)) by YELLOW_4: 21;

      hence thesis by A1;

    end;

    theorem :: WAYBEL14:13

    for P be with_infima Poset, x,y be Element of P holds (( waybelow x) "/\" ( waybelow y)) c= ( downarrow (x "/\" y))

    proof

      let R be with_infima Poset, x,y be Element of R;

      ( {x} "/\" {y}) = {(x "/\" y)} & (( downarrow x) "/\" ( downarrow y)) c= ( downarrow (( downarrow x) "/\" ( downarrow y))) by WAYBEL_0: 16, YELLOW_4: 46;

      then

       A1: (( downarrow x) "/\" ( downarrow y)) c= ( downarrow (x "/\" y)) by YELLOW_4: 62;

      ( waybelow x) c= ( downarrow x) & ( waybelow y) c= ( downarrow y) by WAYBEL_3: 11;

      then (( waybelow x) "/\" ( waybelow y)) c= (( downarrow x) "/\" ( downarrow y)) by YELLOW_4: 48;

      hence thesis by A1;

    end;

    theorem :: WAYBEL14:14

    

     Th14: for R be with_suprema non empty Poset, l be Element of R holds l is co-prime iff for x,y be Element of R st l <= (x "\/" y) holds l <= x or l <= y

    proof

      let R be with_suprema non empty Poset, l be Element of R;

      hereby

        assume l is co-prime;

        then

         A1: (l ~ ) is prime;

        let x,y be Element of R;

        assume l <= (x "\/" y);

        then

         A2: ((x "\/" y) ~ ) <= (l ~ ) by LATTICE3: 9;

        ((x "\/" y) ~ ) = (x "\/" y) by LATTICE3:def 6

        .= ((x ~ ) "/\" (y ~ )) by YELLOW_7: 23;

        then (x ~ ) <= (l ~ ) or (y ~ ) <= (l ~ ) by A1, A2;

        hence l <= x or l <= y by LATTICE3: 9;

      end;

      assume

       A3: for x,y be Element of R st l <= (x "\/" y) holds l <= x or l <= y;

      let x,y be Element of (R ~ );

      

       A4: ( ~ (x "/\" y)) = (x "/\" y) by LATTICE3:def 7

      .= (( ~ x) "\/" ( ~ y)) by YELLOW_7: 24;

      assume (x "/\" y) <= (l ~ );

      then l <= (( ~ x) "\/" ( ~ y)) by A4, YELLOW_7: 2;

      then l <= ( ~ x) or l <= ( ~ y) by A3;

      hence x <= (l ~ ) or y <= (l ~ ) by YELLOW_7: 2;

    end;

    theorem :: WAYBEL14:15

    

     Th15: for P be complete non empty Poset, V be non empty Subset of P holds ( downarrow ( inf V)) = ( meet { ( downarrow u) where u be Element of P : u in V })

    proof

      let P be complete non empty Poset, V be non empty Subset of P;

      set F = { ( downarrow u) where u be Element of P : u in V };

      consider u be object such that

       A1: u in V by XBOOLE_0:def 1;

      

       A2: F c= ( bool the carrier of P)

      proof

        let X be object;

        assume X in F;

        then ex u be Element of P st X = ( downarrow u) & u in V;

        hence thesis;

      end;

      reconsider u as Element of P by A1;

      

       A3: ( downarrow u) in F by A1;

      reconsider F as Subset-Family of P by A2;

      reconsider F as Subset-Family of P;

      now

        let x be object;

        hereby

          assume

           A4: x in ( downarrow ( inf V));

          then

          reconsider d = x as Element of P;

          

           A5: d <= ( inf V) by A4, WAYBEL_0: 17;

          now

            let Y be set;

            assume Y in F;

            then

            consider u be Element of P such that

             A6: Y = ( downarrow u) and

             A7: u in V;

            ( inf V) is_<=_than V by YELLOW_0: 33;

            then ( inf V) <= u by A7, LATTICE3:def 8;

            then d <= u by A5, ORDERS_2: 3;

            hence x in Y by A6, WAYBEL_0: 17;

          end;

          hence x in ( meet F) by A3, SETFAM_1:def 1;

        end;

        assume

         A8: x in ( meet F);

        then

        reconsider d = x as Element of P;

        now

          let b be Element of P;

          assume b in V;

          then ( downarrow b) in F;

          then d in ( downarrow b) by A8, SETFAM_1:def 1;

          hence d <= b by WAYBEL_0: 17;

        end;

        then d is_<=_than V by LATTICE3:def 8;

        then d <= ( inf V) by YELLOW_0: 33;

        hence x in ( downarrow ( inf V)) by WAYBEL_0: 17;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:16

    for P be complete non empty Poset, V be non empty Subset of P holds ( uparrow ( sup V)) = ( meet { ( uparrow u) where u be Element of P : u in V })

    proof

      let P be complete non empty Poset, V be non empty Subset of P;

      set F = { ( uparrow u) where u be Element of P : u in V };

      consider u be object such that

       A1: u in V by XBOOLE_0:def 1;

      

       A2: F c= ( bool the carrier of P)

      proof

        let X be object;

        assume X in F;

        then ex u be Element of P st X = ( uparrow u) & u in V;

        hence thesis;

      end;

      reconsider u as Element of P by A1;

      

       A3: ( uparrow u) in F by A1;

      reconsider F as Subset-Family of P by A2;

      reconsider F as Subset-Family of P;

      now

        let x be object;

        hereby

          assume

           A4: x in ( uparrow ( sup V));

          then

          reconsider d = x as Element of P;

          

           A5: d >= ( sup V) by A4, WAYBEL_0: 18;

          now

            let Y be set;

            assume Y in F;

            then

            consider u be Element of P such that

             A6: Y = ( uparrow u) and

             A7: u in V;

            ( sup V) is_>=_than V by YELLOW_0: 32;

            then ( sup V) >= u by A7, LATTICE3:def 9;

            then d >= u by A5, ORDERS_2: 3;

            hence x in Y by A6, WAYBEL_0: 18;

          end;

          hence x in ( meet F) by A3, SETFAM_1:def 1;

        end;

        assume

         A8: x in ( meet F);

        then

        reconsider d = x as Element of P;

        now

          let b be Element of P;

          assume b in V;

          then ( uparrow b) in F;

          then d in ( uparrow b) by A8, SETFAM_1:def 1;

          hence d >= b by WAYBEL_0: 18;

        end;

        then d is_>=_than V by LATTICE3:def 9;

        then d >= ( sup V) by YELLOW_0: 32;

        hence x in ( uparrow ( sup V)) by WAYBEL_0: 18;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let L be sup-Semilattice, x be Element of L;

      cluster ( compactbelow x) -> directed;

      coherence

      proof

        set cX = ( compactbelow x);

        let xx,yy be Element of L such that

         A1: xx in cX and

         A2: yy in cX;

        set z = (xx "\/" yy);

        yy is compact by A2, WAYBEL_8: 4;

        then yy <= z & yy << yy by YELLOW_0: 22;

        then

         A3: yy << z by WAYBEL_3: 2;

        xx is compact by A1, WAYBEL_8: 4;

        then xx <= z & xx << xx by YELLOW_0: 22;

        then xx << z by WAYBEL_3: 2;

        then z << z by A3, WAYBEL_3: 3;

        then

         A4: z is compact;

        take z;

        xx <= x & yy <= x by A1, A2, WAYBEL_8: 4;

        then z <= x by YELLOW_0: 22;

        hence z in cX by A4;

        thus xx <= z & yy <= z by YELLOW_0: 22;

      end;

    end

    theorem :: WAYBEL14:17

    

     Th17: for T be non empty TopSpace, S be irreducible Subset of T, V be Element of ( InclPoset the topology of T) st V = (S ` ) holds V is prime

    proof

      let T be non empty TopSpace, S be irreducible Subset of T, V be Element of ( InclPoset the topology of T) such that

       A1: V = (S ` );

      set sL = the topology of T;

      let X,Y be Element of ( InclPoset sL);

      

       A2: the carrier of ( InclPoset the topology of T) = the topology of T by YELLOW_1: 1;

      then X in sL & Y in sL;

      then

      reconsider X9 = X, Y9 = Y as Subset of T;

      (X9 /\ Y9) in sL by A2, PRE_TOPC:def 1;

      then

       A3: (X /\ Y) = (X "/\" Y) by YELLOW_1: 9;

      assume (X "/\" Y) <= V;

      then (X /\ Y) c= V by A3, YELLOW_1: 3;

      then S c= ((X9 /\ Y9) ` ) by A1, Lm1;

      then S c= ((X9 ` ) \/ (Y9 ` )) by XBOOLE_1: 54;

      then S = (((X9 ` ) \/ (Y9 ` )) /\ S) by XBOOLE_1: 28;

      then

       A4: S = (((X9 ` ) /\ S) \/ ((Y9 ` ) /\ S)) by XBOOLE_1: 23;

      

       A5: S is closed by YELLOW_8:def 3;

      Y9 is open by A2, PRE_TOPC:def 2;

      then (Y9 ` ) is closed;

      then

       A6: ((Y9 ` ) /\ S) is closed by A5;

      X9 is open by A2, PRE_TOPC:def 2;

      then (X9 ` ) is closed;

      then ((X9 ` ) /\ S) is closed by A5;

      then S = ((X9 ` ) /\ S) or S = ((Y9 ` ) /\ S) by A6, A4, YELLOW_8:def 3;

      then S c= (X9 ` ) or S c= (Y9 ` ) by XBOOLE_1: 17;

      then X c= V or Y c= V by A1, Lm1;

      hence X <= V or Y <= V by YELLOW_1: 3;

    end;

    theorem :: WAYBEL14:18

    

     Th18: for T be non empty TopSpace, x,y be Element of ( InclPoset the topology of T) holds (x "\/" y) = (x \/ y) & (x "/\" y) = (x /\ y)

    proof

      let T be non empty TopSpace, x,y be Element of ( InclPoset the topology of T);

      

       A1: the carrier of ( InclPoset the topology of T) = the topology of T by YELLOW_1: 1;

      then x in the topology of T & y in the topology of T;

      then

      reconsider x9 = x, y9 = y as Subset of T;

      x9 is open & y9 is open by A1, PRE_TOPC:def 2;

      then (x9 \/ y9) is open;

      then (x9 \/ y9) in the topology of T by PRE_TOPC:def 2;

      hence (x "\/" y) = (x \/ y) by YELLOW_1: 8;

      (x9 /\ y9) in the topology of T by A1, PRE_TOPC:def 1;

      hence thesis by YELLOW_1: 9;

    end;

    theorem :: WAYBEL14:19

    

     Th19: for T be non empty TopSpace, V be Element of ( InclPoset the topology of T) holds V is prime iff for X,Y be Element of ( InclPoset the topology of T) st (X /\ Y) c= V holds X c= V or Y c= V

    proof

      let T be non empty TopSpace, V be Element of ( InclPoset the topology of T);

      hereby

        assume

         A1: V is prime;

        let X,Y be Element of ( InclPoset the topology of T);

        assume

         A2: (X /\ Y) c= V;

        (X /\ Y) = (X "/\" Y) by Th18;

        then (X "/\" Y) <= V by A2, YELLOW_1: 3;

        then X <= V or Y <= V by A1;

        hence X c= V or Y c= V by YELLOW_1: 3;

      end;

      assume

       A3: for X,Y be Element of ( InclPoset the topology of T) st (X /\ Y) c= V holds X c= V or Y c= V;

      let X,Y be Element of ( InclPoset the topology of T) such that

       A4: (X "/\" Y) <= V;

      (X /\ Y) = (X "/\" Y) by Th18;

      then (X /\ Y) c= V by A4, YELLOW_1: 3;

      then X c= V or Y c= V by A3;

      hence X <= V or Y <= V by YELLOW_1: 3;

    end;

    theorem :: WAYBEL14:20

    for T be non empty TopSpace, V be Element of ( InclPoset the topology of T) holds V is co-prime iff for X,Y be Element of ( InclPoset the topology of T) st V c= (X \/ Y) holds V c= X or V c= Y

    proof

      let T be non empty TopSpace, V be Element of ( InclPoset the topology of T);

      hereby

        assume

         A1: V is co-prime;

        let X,Y be Element of ( InclPoset the topology of T);

        assume

         A2: V c= (X \/ Y);

        (X \/ Y) = (X "\/" Y) by Th18;

        then V <= (X "\/" Y) by A2, YELLOW_1: 3;

        then V <= X or V <= Y by A1, Th14;

        hence V c= X or V c= Y by YELLOW_1: 3;

      end;

      assume

       A3: for X,Y be Element of ( InclPoset the topology of T) st V c= (X \/ Y) holds V c= X or V c= Y;

      now

        let X,Y be Element of ( InclPoset the topology of T) such that

         A4: V <= (X "\/" Y);

        (X \/ Y) = (X "\/" Y) by Th18;

        then V c= (X \/ Y) by A4, YELLOW_1: 3;

        then V c= X or V c= Y by A3;

        hence V <= X or V <= Y by YELLOW_1: 3;

      end;

      hence thesis by Th14;

    end;

    registration

      let T be non empty TopSpace;

      cluster ( InclPoset the topology of T) -> distributive;

      coherence

      proof

        let x,y,z be Element of ( InclPoset the topology of T);

        

        thus (x "/\" (y "\/" z)) = (x /\ (y "\/" z)) by Th18

        .= (x /\ (y \/ z)) by Th18

        .= ((x /\ y) \/ (x /\ z)) by XBOOLE_1: 23

        .= ((x "/\" y) \/ (x /\ z)) by Th18

        .= ((x "/\" y) \/ (x "/\" z)) by Th18

        .= ((x "/\" y) "\/" (x "/\" z)) by Th18;

      end;

    end

    theorem :: WAYBEL14:21

    

     Th21: for T be non empty TopSpace, L be TopLattice, t be Point of T, l be Point of L, X be Subset-Family of L st the TopStruct of T = the TopStruct of L & t = l & X is Basis of l holds X is Basis of t

    proof

      let T be non empty TopSpace, L be TopLattice, t be Point of T, l be Point of L, X be Subset-Family of L;

      assume

       A1: the TopStruct of T = the TopStruct of L;

      then

      reconsider X9 = X as Subset-Family of T;

      assume

       A2: t = l;

      assume

       A3: X is Basis of l;

      then

       A4: X c= the topology of L by TOPS_2: 64;

      

       A5: l in ( Intersect X) by A3, YELLOW_8:def 1;

      

       A6: for S be Subset of L st S is open & l in S holds ex V be Subset of L st V in X & V c= S by A3, YELLOW_8:def 1;

      now

        let S be Subset of T such that

         A7: S is open and

         A8: t in S;

        reconsider S9 = S as Subset of L by A1;

        S in the topology of T by A7, PRE_TOPC:def 2;

        then S9 is open by A1, PRE_TOPC:def 2;

        then

        consider V be Subset of L such that

         A9: V in X & V c= S9 by A2, A6, A8;

        reconsider V as Subset of T by A1;

        take V;

        thus V in X9 & V c= S by A9;

      end;

      hence thesis by A1, A2, A4, A5, TOPS_2: 64, YELLOW_8:def 1;

    end;

    theorem :: WAYBEL14:22

    

     Th22: for L be TopLattice, x be Element of L st for X be Subset of L st X is open holds X is upper holds ( uparrow x) is compact

    proof

      let L be TopLattice, x be Element of L such that

       A1: for X be Subset of L st X is open holds X is upper;

      set P = ( uparrow x);

      let F be Subset-Family of L such that

       A2: F is Cover of P and

       A3: F is open;

      x <= x;

      then

       A4: x in P by WAYBEL_0: 18;

      P c= ( union F) by A2, SETFAM_1:def 11;

      then

      consider Y be set such that

       A5: x in Y and

       A6: Y in F by A4, TARSKI:def 4;

      reconsider Y as Subset of L by A6;

      reconsider G = {Y} as Subset-Family of L;

      reconsider G as Subset-Family of L;

      take G;

      thus G c= F by A6, ZFMISC_1: 31;

      Y is open by A3, A6;

      then Y is upper by A1;

      then P c= Y by A5, WAYBEL11: 42;

      hence P c= ( union G) by ZFMISC_1: 25;

      thus thesis;

    end;

    begin

    reserve L for complete Scott TopLattice,

x for Element of L,

X,Y for Subset of L,

V,W for Element of ( InclPoset ( sigma L)),

VV for Subset of ( InclPoset ( sigma L));

    registration

      let L be complete LATTICE;

      cluster ( sigma L) -> non empty;

      coherence

      proof

        ( sigma L) = the topology of ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11:def 12;

        hence thesis;

      end;

    end

    theorem :: WAYBEL14:23

    

     Th23: ( sigma L) = the topology of L

    proof

       the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32;

      hence thesis by WAYBEL11:def 12;

    end;

    theorem :: WAYBEL14:24

    

     Th24: X in ( sigma L) iff X is open

    proof

      ( sigma L) = the topology of L by Th23;

      hence thesis by PRE_TOPC:def 2;

    end;

    

     Lm2: for L be complete Scott TopLattice, V be filtered Subset of L, F be Subset-Family of L, CF be Subset of ( InclPoset ( sigma L)) st F = { ( downarrow u) where u be Element of L : u in V } & CF = ( COMPLEMENT F) holds CF is directed

    proof

      let L be complete Scott TopLattice, V be filtered Subset of L, F be Subset-Family of L, CF be Subset of ( InclPoset ( sigma L)) such that

       A1: F = { ( downarrow u) where u be Element of L : u in V } and

       A2: CF = ( COMPLEMENT F);

      set IPs = ( InclPoset ( sigma L));

      let x,y be Element of IPs such that

       A3: x in CF and

       A4: y in CF;

      

       A5: ( sigma L) = the topology of L by Th23;

      then

       A6: the carrier of IPs = the topology of L by YELLOW_1: 1;

      then x in ( sigma L) & y in ( sigma L) by A5;

      then

      reconsider x9 = x, y9 = y as Subset of L;

      (x9 ` ) in F by A2, A3, SETFAM_1:def 7;

      then

      consider ux be Element of L such that

       A7: (x9 ` ) = ( downarrow ux) and

       A8: ux in V by A1;

      (y9 ` ) in F by A2, A4, SETFAM_1:def 7;

      then

      consider uy be Element of L such that

       A9: (y9 ` ) = ( downarrow uy) and

       A10: uy in V by A1;

      consider uz be Element of L such that

       A11: uz in V and

       A12: uz <= ux and

       A13: uz <= uy by A8, A10, WAYBEL_0:def 2;

      (( downarrow uz) ` ) is open by WAYBEL11: 12;

      then

      reconsider z = (( downarrow uz) ` ) as Element of IPs by A6, PRE_TOPC:def 2;

      take z;

      ( downarrow uz) in F by A1, A11;

      hence z in CF by A2, YELLOW_8: 5;

      ( downarrow uz) c= ( downarrow uy) by A13, WAYBEL_0: 21;

      then

       A14: (( downarrow uy) ` ) c= (( downarrow uz) ` ) by SUBSET_1: 12;

      ( downarrow uz) c= ( downarrow ux) by A12, WAYBEL_0: 21;

      then (( downarrow ux) ` ) c= (( downarrow uz) ` ) by SUBSET_1: 12;

      hence x <= z & y <= z by A7, A9, A14, YELLOW_1: 3;

    end;

    theorem :: WAYBEL14:25

    

     Th25: for X be filtered Subset of L st VV = { (( downarrow x) ` ) : x in X } holds VV is directed

    proof

      let V be filtered Subset of L;

      set F = { ( downarrow u) where u be Element of L : u in V };

      F c= ( bool the carrier of L)

      proof

        let x be object;

        assume x in F;

        then ex u be Element of L st x = ( downarrow u) & u in V;

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of L;

      reconsider F as Subset-Family of L;

      assume

       A1: VV = { (( downarrow x) ` ) : x in V };

      VV c= ( bool the carrier of L)

      proof

        let x be object;

        assume x in VV;

        then ex u be Element of L st x = (( downarrow u) ` ) & u in V by A1;

        hence thesis;

      end;

      then

      reconsider VV as Subset-Family of L;

      reconsider VV as Subset-Family of L;

      now

        let x be object;

        hereby

          assume x in VV;

          then

          consider u be Element of L such that

           A2: x = (( downarrow u) ` ) and

           A3: u in V by A1;

          ( downarrow u) in F by A3;

          hence x in ( COMPLEMENT F) by A2, YELLOW_8: 5;

        end;

        assume

         A4: x in ( COMPLEMENT F);

        then

        reconsider X = x as Subset of L;

        (X ` ) in F by A4, SETFAM_1:def 7;

        then

        consider u be Element of L such that

         A5: (X ` ) = ( downarrow u) and

         A6: u in V;

        X = (( downarrow u) ` ) by A5;

        hence x in VV by A1, A6;

      end;

      then VV = ( COMPLEMENT F) by TARSKI: 2;

      hence thesis by Lm2;

    end;

    theorem :: WAYBEL14:26

    

     Th26: X is open & x in X implies ( inf X) << x

    proof

      assume that

       A1: X is open and

       A2: x in X;

      

       A3: X is upper property(S) by A1, WAYBEL11: 15;

      now

        let D be non empty directed Subset of L;

        assume x <= ( sup D);

        then ( sup D) in X by A2, A3;

        then

        consider y be Element of L such that

         A4: y in D and

         A5: for x be Element of L st x in D & x >= y holds x in X by A3, WAYBEL11:def 3;

        take y;

        thus y in D by A4;

        y <= y;

        then ( inf X) is_<=_than X & y in X by A4, A5, YELLOW_0: 33;

        hence ( inf X) <= y by LATTICE3:def 8;

      end;

      hence thesis;

    end;

    definition

      let R be non empty reflexive RelStr, f be Function of [:R, R:], R;

      :: WAYBEL14:def1

      attr f is jointly_Scott-continuous means for T be non empty TopSpace st the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence R)) holds ex ft be Function of [:T, T:], T st ft = f & ft is continuous;

    end

    theorem :: WAYBEL14:27

    

     Th27: V = X implies (V is co-prime iff X is filtered upper)

    proof

      assume

       A1: V = X;

      

       A2: the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32;

      

       A3: ( sigma L) = the topology of ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11:def 12;

      

       A4: the carrier of ( InclPoset ( sigma L)) = ( sigma L) by YELLOW_1: 1;

      then

       A5: X is upper by A1, A3, WAYBEL11: 31;

      hereby

        assume

         A6: V is co-prime;

        thus X is filtered

        proof

          let v,w be Element of L such that

           A7: v in X and

           A8: w in X;

          (( downarrow w) ` ) is open & (( downarrow v) ` ) is open by WAYBEL11: 12;

          then

          reconsider mdw = (( downarrow w) ` ), mdv = (( downarrow v) ` ) as Element of ( InclPoset ( sigma L)) by A3, A4, A2, PRE_TOPC:def 2;

          w <= w;

          then w in ( downarrow w) by WAYBEL_0: 17;

          then not V c= (( downarrow w) ` ) by A1, A8, XBOOLE_0:def 5;

          then

           A9: not V <= mdw by YELLOW_1: 3;

          v <= v;

          then v in ( downarrow v) by WAYBEL_0: 17;

          then not V c= (( downarrow v) ` ) by A1, A7, XBOOLE_0:def 5;

          then not V <= mdv by YELLOW_1: 3;

          then not V <= (mdv "\/" mdw) by A3, A6, A9, Th14;

          then

           A10: not V c= (mdv "\/" mdw) by YELLOW_1: 3;

          take z = (v "/\" w);

          

           A11: (mdv \/ mdw) = ((( downarrow v) /\ ( downarrow w)) ` ) by XBOOLE_1: 54

          .= (( downarrow (v "/\" w)) ` ) by Th3;

          (mdv \/ mdw) c= (mdv "\/" mdw) by A3, YELLOW_1: 6;

          then not V c= (mdv \/ mdw) by A10;

          then X meets ((( downarrow (v "/\" w)) ` ) ` ) by A1, A11, SUBSET_1: 24;

          then (X /\ ((( downarrow (v "/\" w)) ` ) ` )) <> {} ;

          then

          consider zz be object such that

           A12: zz in (X /\ ( downarrow (v "/\" w))) by XBOOLE_0:def 1;

          

           A13: zz in ( downarrow (v "/\" w)) by A12, XBOOLE_0:def 4;

          

           A14: zz in X by A12, XBOOLE_0:def 4;

          reconsider zz as Element of L by A12;

          zz <= (v "/\" w) by A13, WAYBEL_0: 17;

          hence z in X by A5, A14;

          thus z <= v & z <= w by YELLOW_0: 23;

        end;

        thus X is upper by A1, A3, A4, WAYBEL11: 31;

      end;

      assume

       A15: X is filtered upper;

      assume not V is co-prime;

      then

      consider Xx,Y be Element of ( InclPoset ( sigma L)) such that

       A16: V <= (Xx "\/" Y) and

       A17: not V <= Xx and

       A18: not V <= Y by A3, Th14;

      Xx in ( sigma L) & Y in ( sigma L) by A4;

      then

      reconsider Xx9 = Xx, Y9 = Y as Subset of L;

      

       A19: Y9 is open by A3, A4, A2, PRE_TOPC:def 2;

      then

       A20: Y9 is upper by WAYBEL11:def 4;

      

       A21: Xx9 is open by A3, A4, A2, PRE_TOPC:def 2;

      then (Xx9 \/ Y9) is open by A19;

      then (Xx \/ Y) in ( sigma L) by A3, A2, PRE_TOPC:def 2;

      then (Xx \/ Y) = (Xx "\/" Y) by YELLOW_1: 8;

      then

       A22: V c= (Xx \/ Y) by A16, YELLOW_1: 3;

       not V c= Y by A18, YELLOW_1: 3;

      then

      consider w be object such that

       A23: w in V and

       A24: not w in Y;

       not V c= Xx by A17, YELLOW_1: 3;

      then

      consider v be object such that

       A25: v in V and

       A26: not v in Xx;

      reconsider v, w as Element of L by A1, A25, A23;

      

       A27: Xx9 is upper by A21, WAYBEL11:def 4;

       A28:

      now

        assume

         A29: (v "/\" w) in (Xx9 \/ Y9);

        per cases by A29, XBOOLE_0:def 3;

          suppose

           A30: (v "/\" w) in Xx9;

          (v "/\" w) <= v by YELLOW_0: 23;

          hence contradiction by A26, A27, A30;

        end;

          suppose

           A31: (v "/\" w) in Y9;

          (v "/\" w) <= w by YELLOW_0: 23;

          hence contradiction by A24, A20, A31;

        end;

      end;

      (v "/\" w) in X by A1, A15, A25, A23, WAYBEL_0: 41;

      hence contradiction by A1, A22, A28;

    end;

    theorem :: WAYBEL14:28

    (V = X & ex x st X = (( downarrow x) ` )) implies V is prime & V <> the carrier of L

    proof

      assume

       A1: V = X;

      

       A2: ( sigma L) = the topology of ( ConvergenceSpace ( Scott-Convergence L)) & the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32, WAYBEL11:def 12;

      given u be Element of L such that

       A3: X = (( downarrow u) ` );

      ( Cl {u}) = ( downarrow u) & ( Cl {u}) is irreducible by WAYBEL11: 9, YELLOW_8: 17;

      hence V is prime by A1, A2, A3, Th17;

      assume V = the carrier of L;

      hence contradiction by A1, A3, Th2;

    end;

    theorem :: WAYBEL14:29

    

     Th29: V = X & ( sup_op L) is jointly_Scott-continuous & V is prime & V <> the carrier of L implies ex x st X = (( downarrow x) ` )

    proof

      assume that

       A1: V = X and

       A2: ( sup_op L) is jointly_Scott-continuous and

       A3: V is prime and

       A4: V <> the carrier of L;

      

       A5: the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32;

      set A = (X ` );

      

       A6: ( sigma L) = the topology of ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11:def 12;

      

       A7: the carrier of ( InclPoset ( sigma L)) = ( sigma L) by YELLOW_1: 1;

      then

       A8: X is open by A1, A6, A5, PRE_TOPC:def 2;

      then A is closed;

      then

       A9: A is directly_closed lower by WAYBEL11: 7;

      

       A10: A is directed

      proof

        set LxL = [:L qua non empty TopSpace, L:];

        given a,b be Element of L such that

         A11: a in A & b in A and

         A12: for z be Element of L holds not (z in A & a <= z & b <= z);

        a <= (a "\/" b) & b <= (a "\/" b) by YELLOW_0: 22;

        then not (a "\/" b) in A by A12;

        then

         A13: (a "\/" b) in X by XBOOLE_0:def 5;

        consider Tsup be Function of LxL, L such that

         A14: Tsup = ( sup_op L) and

         A15: Tsup is continuous by A2, A5;

        

         A16: (Tsup . (a,b)) = (a "\/" b) by A14, WAYBEL_2:def 5;

        ( [#] L) <> {} ;

        then (Tsup " X) is open by A8, A15, TOPS_2: 43;

        then

        consider AA be Subset-Family of LxL such that

         A17: (Tsup " X) = ( union AA) and

         A18: for e be set st e in AA holds ex X1 be Subset of L, Y1 be Subset of L st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

        

         A19: the carrier of LxL = [:the carrier of L, the carrier of L:] by BORSUK_1:def 2;

        then [a, b] in the carrier of LxL by ZFMISC_1:def 2;

        then [a, b] in (Tsup " X) by A13, A16, FUNCT_2: 38;

        then

        consider AAe be set such that

         A20: [a, b] in AAe and

         A21: AAe in AA by A17, TARSKI:def 4;

        consider Va,Vb be Subset of L such that

         A22: AAe = [:Va, Vb:] and

         A23: Va is open and

         A24: Vb is open by A18, A21;

        

         A25: a in Va & b in Vb by A20, A22, ZFMISC_1: 87;

        reconsider Va9 = Va, Vb9 = Vb as Subset of L;

        now

          let x be object;

          hereby

            assume x in (Tsup .: AAe);

            then

            consider cd be object such that

             A26: cd in the carrier of LxL and

             A27: cd in AAe and

             A28: (Tsup . cd) = x by FUNCT_2: 64;

            consider c,d be Element of L such that

             A29: cd = [c, d] by A19, A26, DOMAIN_1: 1;

            reconsider c, d as Element of L;

            

             A30: x = (Tsup . (c,d)) by A28, A29

            .= (c "\/" d) by A14, WAYBEL_2:def 5;

            

             A31: d <= (c "\/" d) & Vb9 is upper by A24, WAYBEL11:def 4, YELLOW_0: 22;

            d in Vb by A22, A27, A29, ZFMISC_1: 87;

            then

             A32: x in Vb by A30, A31;

            

             A33: c <= (c "\/" d) & Va9 is upper by A23, WAYBEL11:def 4, YELLOW_0: 22;

            c in Va by A22, A27, A29, ZFMISC_1: 87;

            then x in Va by A30, A33;

            hence x in (Va /\ Vb) by A32, XBOOLE_0:def 4;

          end;

          assume

           A34: x in (Va /\ Vb);

          then

          reconsider c = x as Element of L;

          x in Va & x in Vb by A34, XBOOLE_0:def 4;

          then

           A35: [c, c] in AAe by A22, ZFMISC_1: 87;

          c <= c;

          then c = (c "\/" c) by YELLOW_0: 24;

          then

           A36: c = (Tsup . (c,c)) by A14, WAYBEL_2:def 5;

           [c, c] in the carrier of LxL by A19, ZFMISC_1: 87;

          hence x in (Tsup .: AAe) by A35, A36, FUNCT_2: 35;

        end;

        then

         A37: (Tsup .: AAe) = (Va /\ Vb) by TARSKI: 2;

        

         A38: (Tsup .: (Tsup " X)) c= X by FUNCT_1: 75;

        (Tsup .: AAe) c= (Tsup .: (Tsup " X)) by A17, A21, RELAT_1: 123, ZFMISC_1: 74;

        then

         A39: (Tsup .: AAe) c= X by A38;

        Va in ( sigma L) & Vb in ( sigma L) by A6, A5, A23, A24, PRE_TOPC:def 2;

        then Va c= X or Vb c= X by A1, A3, A6, A7, A37, A39, Th19;

        hence contradiction by A11, A25, XBOOLE_0:def 5;

      end;

      take u = ( sup A);

      now

        assume A = {} ;

        then (A ` ) = the carrier of L;

        hence contradiction by A1, A4;

      end;

      then u in A by A9, A10, WAYBEL11:def 2;

      then A = ( downarrow u) by A9, Th5;

      hence thesis;

    end;

    theorem :: WAYBEL14:30

    

     Th30: L is continuous implies ( sup_op L) is jointly_Scott-continuous

    proof

      assume

       A1: L is continuous;

      set Tsup = ( sup_op L);

      let T be non empty TopSpace such that

       A2: the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence L));

      

       A3: the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] by BORSUK_1:def 2;

      

       A4: the carrier of T = the carrier of L by A2, YELLOW_6:def 24;

      then the carrier of [:T, T:] = the carrier of [:L, L:] by A3, YELLOW_3:def 2;

      then

      reconsider Tsup as Function of [:T, T:], T by A4;

      take Tsup;

      thus Tsup = ( sup_op L);

      

       A5: the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32;

      for x be Point of [:T, T:] holds Tsup is_continuous_at x

      proof

        reconsider Lc = L as continuous complete Scott TopLattice by A1;

        let ab be Point of [:T, T:];

        reconsider Tsab = (Tsup . ab) as Point of T;

        consider a,b be Point of T such that

         A6: ab = [a, b] by A3, DOMAIN_1: 1;

        reconsider a9 = a, b9 = b as Element of L by A2, YELLOW_6:def 24;

        set D1 = ( waybelow a9), D2 = ( waybelow b9);

        set D = (D1 "\/" D2);

        reconsider Tsab9 = Tsab as Element of L by A2, YELLOW_6:def 24;

        let G be a_neighborhood of (Tsup . ab);

        

         A7: Tsab in ( Int G) by CONNSP_2:def 1;

        reconsider basab = { ( wayabove q) where q be Element of L : q << Tsab9 } as Basis of Tsab9 by A1, WAYBEL11: 44;

        basab is Basis of Tsab by A2, A5, Th21;

        then

        consider V be Subset of T such that

         A8: V in basab and

         A9: V c= ( Int G) by A7, YELLOW_8:def 1;

        consider u be Element of L such that

         A10: V = ( wayabove u) and

         A11: u << Tsab9 by A8;

        

         A12: D = { (x "\/" y) where x,y be Element of L : x in D1 & y in D2 } by YELLOW_4:def 3;

        Lc = L;

        then

         A13: a9 = ( sup ( waybelow a9)) & b9 = ( sup ( waybelow b9)) by WAYBEL_3:def 5;

        Tsab9 = (Tsup . (a,b)) by A6

        .= (a9 "\/" b9) by WAYBEL_2:def 5

        .= ( sup (( waybelow a9) "\/" ( waybelow b9))) by A13, WAYBEL_2: 4;

        then

        consider xy be Element of L such that

         A14: xy in D and

         A15: u << xy by A1, A11, WAYBEL_4: 53;

        consider x,y be Element of L such that

         A16: xy = (x "\/" y) and

         A17: x in D1 and

         A18: y in D2 by A14, A12;

        reconsider H = [:( wayabove x), ( wayabove y):] as Subset of [:T, T:] by A4, A3, YELLOW_3:def 2;

        y << b9 by A18, WAYBEL_3: 7;

        then

         A19: b9 in ( wayabove y);

        ( Int G) c= G by TOPS_1: 16;

        then

         A20: V c= G by A9;

        reconsider wx = ( wayabove x), wy = ( wayabove y) as Subset of T by A2, YELLOW_6:def 24;

        ( wayabove y) is open by A1, WAYBEL11: 36;

        then ( wayabove y) in the topology of L by PRE_TOPC:def 2;

        then

         A21: wy is open by A2, A5, PRE_TOPC:def 2;

        ( wayabove x) is open by A1, WAYBEL11: 36;

        then ( wayabove x) in the topology of L by PRE_TOPC:def 2;

        then wx is open by A2, A5, PRE_TOPC:def 2;

        then H is open by A21, BORSUK_1: 6;

        then

         A22: H = ( Int H) by TOPS_1: 23;

        x << a9 by A17, WAYBEL_3: 7;

        then a9 in ( wayabove x);

        then [a9, b9] in H by A19, ZFMISC_1: 87;

        then

        reconsider H as a_neighborhood of ab by A6, A22, CONNSP_2:def 1;

        take H;

        

         A23: (Tsup .: H) = (( wayabove x) "\/" ( wayabove y)) & (( wayabove x) "\/" ( wayabove y)) c= ( uparrow (x "\/" y)) by Th12, WAYBEL_2: 35;

        ( uparrow (x "\/" y)) c= ( wayabove u) by A15, A16, Th7;

        then (Tsup .: H) c= V by A10, A23;

        hence thesis by A20;

      end;

      hence thesis by TMAP_1: 44;

    end;

    theorem :: WAYBEL14:31

    

     Th31: ( sup_op L) is jointly_Scott-continuous implies L is sober

    proof

      assume

       A1: ( sup_op L) is jointly_Scott-continuous;

      let S be irreducible Subset of L;

      

       A2: ( sigma L) = the topology of ( ConvergenceSpace ( Scott-Convergence L)) & the TopStruct of L = ( ConvergenceSpace ( Scott-Convergence L)) by WAYBEL11: 32, WAYBEL11:def 12;

      

       A3: S is non empty closed by YELLOW_8:def 3;

      then the carrier of ( InclPoset ( sigma L)) = ( sigma L) & (S ` ) is open by YELLOW_1: 1;

      then

      reconsider V = (S ` ) as Element of ( InclPoset ( sigma L)) by A2, PRE_TOPC:def 2;

      (S ` ) <> the carrier of L by Th2;

      then

      consider p be Element of L such that

       A4: V = (( downarrow p) ` ) by A1, A2, Th17, Th29;

      

       A5: L is T_0 by WAYBEL11: 10;

      take p;

      

       A6: ( Cl {p}) = ( downarrow p) by WAYBEL11: 9;

      

       A7: S = ( downarrow p) by A4, TOPS_1: 1;

      hence p is_dense_point_of S by A6, YELLOW_8: 18;

      let q be Point of L;

      assume q is_dense_point_of S;

      then ( Cl {q}) = S by A3, YELLOW_8: 16;

      hence thesis by A7, A6, A5, YELLOW_8: 23;

    end;

    theorem :: WAYBEL14:32

    L is continuous implies L is compact locally-compact sober Baire

    proof

      assume

       A1: L is continuous;

      

       A2: ( uparrow ( Bottom L)) = the carrier of L & ( [#] L) = the carrier of L by Th10;

      

       A3: for X be Subset of L st X is open holds X is upper by WAYBEL11:def 4;

      then ( uparrow ( Bottom L)) is compact by Th22;

      hence L is compact by A2;

      thus

       A4: L is locally-compact

      proof

        let x be Point of L, X be Subset of L such that

         A5: x in X and

         A6: X is open;

        reconsider x9 = x as Element of L;

        consider y be Element of L such that

         A7: y << x9 and

         A8: y in X by A1, A5, A6, WAYBEL11: 43;

        set Y = ( uparrow y);

        set bas = { ( wayabove q) where q be Element of L : q << x9 };

        

         A9: bas is Basis of x by A1, WAYBEL11: 44;

        ( wayabove y) in bas by A7;

        then ( wayabove y) is open by A9, YELLOW_8: 12;

        then

         A10: ( wayabove y) c= ( Int Y) by TOPS_1: 24, WAYBEL_3: 11;

        take Y;

        x in ( wayabove y) by A7;

        hence x in ( Int Y) by A10;

        X is upper by A6, WAYBEL11:def 4;

        hence Y c= X by A8, WAYBEL11: 42;

        thus thesis by A3, Th22;

      end;

      ( sup_op L) is jointly_Scott-continuous by A1, Th30;

      hence L is sober by Th31;

      hence thesis by A4, WAYBEL12: 44;

    end;

    theorem :: WAYBEL14:33

    

     Th33: L is continuous & X in ( sigma L) implies X = ( union { ( wayabove x) : x in X })

    proof

      assume that

       A1: L is continuous and

       A2: X in ( sigma L);

      set WAV = { ( wayabove x) where x be Element of L : x in X };

      

       A3: X is open by A2, Th24;

      now

        let x be object;

        hereby

          assume

           A4: x in X;

          then

          reconsider x9 = x as Element of L;

          consider q be Element of L such that

           A5: q << x9 & q in X by A1, A3, A4, WAYBEL11: 43;

          x9 in ( wayabove q) & ( wayabove q) in WAV by A5;

          hence x in ( union WAV) by TARSKI:def 4;

        end;

        assume x in ( union WAV);

        then

        consider Y be set such that

         A6: x in Y and

         A7: Y in WAV by TARSKI:def 4;

        consider q be Element of L such that

         A8: Y = ( wayabove q) and

         A9: q in X by A7;

        

         A10: ( wayabove q) c= ( uparrow q) by WAYBEL_3: 11;

        X is upper by A3, WAYBEL11:def 4;

        then ( uparrow q) c= X by A9, WAYBEL11: 42;

        then Y c= X by A8, A10;

        hence x in X by A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL14:34

    (for X st X in ( sigma L) holds X = ( union { ( wayabove x) : x in X })) implies L is continuous

    proof

      assume

       A1: for X be Subset of L st X in ( sigma L) holds X = ( union { ( wayabove x) where x be Element of L : x in X });

      thus for x be Element of L holds ( waybelow x) is non empty directed;

      thus L is up-complete;

      let x be Element of L;

      set y = ( sup ( waybelow x)), X = (( downarrow y) ` );

      assume

       A2: x <> ( sup ( waybelow x));

      

       A3: y <= x by Th9;

      now

        assume x in ( downarrow y);

        then x <= y by WAYBEL_0: 17;

        hence contradiction by A3, A2, ORDERS_2: 2;

      end;

      then

       A4: x in X by XBOOLE_0:def 5;

      set Z = { ( wayabove z) where z be Element of L : z in X };

      

       A5: y is_>=_than ( waybelow x) by YELLOW_0: 32;

      X is open by WAYBEL11: 12;

      then X in ( sigma L) by Th24;

      then X = ( union Z) by A1;

      then

      consider Y be set such that

       A6: x in Y and

       A7: Y in Z by A4, TARSKI:def 4;

      consider z be Element of L such that

       A8: Y = ( wayabove z) and

       A9: z in X by A7;

      z << x by A6, A8, WAYBEL_3: 8;

      then z in ( waybelow x);

      then z <= y by A5, LATTICE3:def 9;

      then z in ( downarrow y) by WAYBEL_0: 17;

      hence contradiction by A9, XBOOLE_0:def 5;

    end;

    theorem :: WAYBEL14:35

    L is continuous implies ex B be Basis of x st for X st X in B holds X is open filtered

    proof

      set B = { V where V be Subset of L : ex q be Element of L st V c= ( wayabove q) & q << x & x in V & V is open filtered };

      B c= ( bool the carrier of L)

      proof

        let X be object;

        assume X in B;

        then ex V be Subset of L st X = V & ex q be Element of L st V c= ( wayabove q) & q << x & x in V & V is open filtered;

        hence thesis;

      end;

      then

      reconsider B as Subset-Family of L;

      reconsider B as Subset-Family of L;

      assume

       A1: L is continuous;

      then

      reconsider A = { ( wayabove q) where q be Element of L : q << x } as Basis of x by WAYBEL11: 44;

      

       A2: B is Basis of x

      proof

        

         A3: B is open

        proof

          let Y be Subset of L;

          assume Y in B;

          then ex V be Subset of L st Y = V & ex q be Element of L st V c= ( wayabove q) & q << x & x in V & V is open filtered;

          hence thesis;

        end;

        B is x -quasi_basis

        proof

          thus x in ( Intersect B)

          proof

            per cases ;

              suppose B is empty;

              then ( Intersect B) = the carrier of L by SETFAM_1:def 9;

              hence thesis;

            end;

              suppose

               A4: B is non empty;

               A5:

              now

                let Y be set;

                assume Y in B;

                then ex V be Subset of L st Y = V & ex q be Element of L st V c= ( wayabove q) & q << x & x in V & V is open filtered;

                hence x in Y;

              end;

              ( Intersect B) = ( meet B) by A4, SETFAM_1:def 9;

              hence thesis by A4, A5, SETFAM_1:def 1;

            end;

          end;

          let S be Subset of L;

          assume S is open & x in S;

          then

          consider V be Subset of L such that

           A6: V in A and

           A7: V c= S by YELLOW_8:def 1;

          consider q be Element of L such that

           A8: V = ( wayabove q) and

           A9: q << x by A6;

          consider F be Open Filter of L such that

           A10: x in F and

           A11: F c= ( wayabove q) by A1, A9, WAYBEL_6: 8;

          take F;

          F is open by WAYBEL11: 41;

          hence F in B by A9, A10, A11;

          thus thesis by A7, A8, A11;

        end;

        hence thesis by A3;

      end;

      now

        let Y be Subset of L;

        assume Y in B;

        then ex V be Subset of L st Y = V & ex q be Element of L st V c= ( wayabove q) & q << x & x in V & V is open filtered;

        hence Y is open filtered;

      end;

      hence thesis by A2;

    end;

    theorem :: WAYBEL14:36

    L is continuous implies ( InclPoset ( sigma L)) is continuous

    proof

      assume

       A1: L is continuous;

      set IPs = ( InclPoset the topology of L);

      

       A2: the carrier of IPs = the topology of L by YELLOW_1: 1;

      

       A3: ( sigma L) = the topology of L by Th23;

      IPs is satisfying_axiom_of_approximation

      proof

        let V be Element of IPs;

        set VV = { ( wayabove x) where x be Element of L : x in V };

        set wV = ( waybelow V);

        V in ( sigma L) by A3, A2;

        then

         A4: V = ( union VV) by A1, Th33;

        now

          let x be object;

          hereby

            assume x in V;

            then

            consider xU be set such that

             A5: x in xU and

             A6: xU in VV by A4, TARSKI:def 4;

            consider y be Element of L such that

             A7: xU = ( wayabove y) and

             A8: y in V by A6;

            ( wayabove y) is open by A1, WAYBEL11: 36;

            then

            reconsider xU as Element of IPs by A2, A7, PRE_TOPC:def 2;

            xU << V

            proof

              let D be non empty directed Subset of IPs;

              assume V <= ( sup D);

              then V c= ( sup D) by YELLOW_1: 3;

              then V c= ( union D) by YELLOW_1: 22;

              then

              consider DD be set such that

               A9: y in DD and

               A10: DD in D by A8, TARSKI:def 4;

              DD in ( sigma L) by A3, A2, A10;

              then

              reconsider DD as Subset of L;

              DD is open by A2, A10, PRE_TOPC:def 2;

              then DD is upper by WAYBEL11:def 4;

              then

               A11: ( uparrow y) c= DD by A9, WAYBEL11: 42;

              reconsider d = DD as Element of IPs by A10;

              take d;

              thus d in D by A10;

              ( wayabove y) c= ( uparrow y) by WAYBEL_3: 11;

              then ( wayabove y) c= DD by A11;

              hence thesis by A7, YELLOW_1: 3;

            end;

            then xU in wV;

            hence x in ( union wV) by A5, TARSKI:def 4;

          end;

          assume x in ( union wV);

          then

          consider X be set such that

           A12: x in X and

           A13: X in wV by TARSKI:def 4;

          reconsider X as Element of IPs by A13;

          X << V by A13, WAYBEL_3: 7;

          then X <= V by WAYBEL_3: 1;

          then X c= V by YELLOW_1: 3;

          hence x in V by A12;

        end;

        then V = ( union ( waybelow V)) by TARSKI: 2;

        hence thesis by YELLOW_1: 22;

      end;

      hence thesis by Th23;

    end;

    theorem :: WAYBEL14:37

    

     Th37: (for x holds ex B be Basis of x st for Y st Y in B holds Y is open filtered) & ( InclPoset ( sigma L)) is continuous implies x = ( "\/" ({ ( inf X) : x in X & X in ( sigma L) },L))

    proof

      assume that

       A1: for x be Element of L holds ex B be Basis of x st for Y be Subset of L st Y in B holds Y is open filtered and

       A2: ( InclPoset ( sigma L)) is continuous;

      

       A3: ( sigma L) = the topology of L by Th23;

      set IU = { ( inf V) where V be Subset of L : x in V & V in ( sigma L) };

      set IPs = ( InclPoset the topology of L);

      

       A4: the carrier of IPs = the topology of L by YELLOW_1: 1;

      set y = ( "\/" (IU,L));

      set VVl = (( downarrow y) ` );

      now

        let b be Element of L;

        assume b in IU;

        then

        consider V be Subset of L such that

         A5: b = ( inf V) and

         A6: x in V and V in ( sigma L);

        b is_<=_than V by A5, YELLOW_0: 33;

        hence b <= x by A6, LATTICE3:def 8;

      end;

      then x is_>=_than IU by LATTICE3:def 9;

      then

       A7: y <= x by YELLOW_0: 32;

      assume

       A8: x <> y;

      now

        assume x in ( downarrow y);

        then x <= y by WAYBEL_0: 17;

        hence contradiction by A7, A8, ORDERS_2: 2;

      end;

      then

       A9: x in VVl by XBOOLE_0:def 5;

      VVl is open by WAYBEL11: 12;

      then

      reconsider VVp = VVl as Element of IPs by A3, A4, Th24;

      VVp = ( sup ( waybelow VVp)) by A2, A3, WAYBEL_3:def 5;

      then VVp = ( union ( waybelow VVp)) by YELLOW_1: 22;

      then

      consider Vp be set such that

       A10: x in Vp and

       A11: Vp in ( waybelow VVp) by A9, TARSKI:def 4;

      reconsider Vp as Element of IPs by A11;

      Vp in ( sigma L) by A3, A4;

      then

      reconsider Vl = Vp as Subset of L;

      

       A12: Vp << VVp by A11, WAYBEL_3: 7;

      consider bas be Basis of x such that

       A13: for Y be Subset of L st Y in bas holds Y is open filtered by A1;

      

       A14: y is_>=_than IU by YELLOW_0: 32;

      Vl is open by A4, PRE_TOPC:def 2;

      then

      consider Ul be Subset of L such that

       A15: Ul in bas and

       A16: Ul c= Vl by A10, YELLOW_8:def 1;

      set F = { ( downarrow u) where u be Element of L : u in Ul };

      

       A17: x in Ul by A15, YELLOW_8: 12;

      then

       A18: ( downarrow x) in F;

      F c= ( bool the carrier of L)

      proof

        let X be object;

        assume X in F;

        then ex u be Element of L st X = ( downarrow u) & u in Ul;

        hence thesis;

      end;

      then

      reconsider F as non empty Subset-Family of L by A18;

      ( COMPLEMENT F) c= the topology of L

      proof

        let X be object;

        assume

         A19: X in ( COMPLEMENT F);

        then

        reconsider X9 = X as Subset of L;

        (X9 ` ) in F by A19, SETFAM_1:def 7;

        then

        consider u be Element of L such that

         A20: (X9 ` ) = ( downarrow u) and u in Ul;

        X9 = (( downarrow u) ` ) by A20;

        then X9 is open by WAYBEL11: 12;

        hence thesis by PRE_TOPC:def 2;

      end;

      then

      reconsider CF = ( COMPLEMENT F) as Subset of IPs by YELLOW_1: 1;

      Ul is filtered by A13, A15;

      then

       A21: CF is directed by A3, Lm2;

      Ul is open by A15, YELLOW_8: 12;

      then Ul in ( sigma L) by A3, PRE_TOPC:def 2;

      then ( inf Ul) in IU by A17;

      then ( inf Ul) <= y by A14, LATTICE3:def 9;

      then ( downarrow ( inf Ul)) c= ( downarrow y) by WAYBEL_0: 21;

      then

       A22: (( downarrow y) ` ) c= (( downarrow ( inf Ul)) ` ) by SUBSET_1: 12;

      ( downarrow ( inf Ul)) = ( meet F) by A17, Th15;

      then (( downarrow ( inf Ul)) ` ) = ( union ( COMPLEMENT F)) by TOPS_2: 7;

      then VVp c= ( sup CF) by A22, YELLOW_1: 22;

      then

       A23: VVp <= ( sup CF) by YELLOW_1: 3;

      (( downarrow x) ` ) in ( COMPLEMENT F) by A18, YELLOW_8: 5;

      then

      consider d be Element of IPs such that

       A24: d in CF and

       A25: Vp << d by A2, A3, A12, A21, A23, WAYBEL_4: 53;

      Vp <= d by A25, WAYBEL_3: 1;

      then

       A26: Vp c= d by YELLOW_1: 3;

      d in ( sigma L) by A3, A4;

      then

      reconsider d9 = d as Subset of L;

      (d9 ` ) in F by A24, SETFAM_1:def 7;

      then

      consider u be Element of L such that

       A27: (d9 ` ) = ( downarrow u) and

       A28: u in Ul;

      u <= u;

      then u in ( downarrow u) by WAYBEL_0: 17;

      then not u in Vp by A27, A26, XBOOLE_0:def 5;

      hence contradiction by A16, A28;

    end;

    theorem :: WAYBEL14:38

    

     Th38: (for x holds x = ( "\/" ({ ( inf X) : x in X & X in ( sigma L) },L))) implies L is continuous

    proof

      assume

       A1: for x be Element of L holds x = ( "\/" ({ ( inf V) where V be Subset of L : x in V & V in ( sigma L) },L));

      thus for x be Element of L holds ( waybelow x) is non empty directed;

      thus L is up-complete;

      let x be Element of L;

      set VV = { ( inf V) where V be Subset of L : x in V & V in ( sigma L) };

      

       A2: ( sup ( waybelow x)) <= x by Th9;

      

       A3: VV c= ( waybelow x)

      proof

        let d be object;

        assume d in VV;

        then

        consider V be Subset of L such that

         A4: ( inf V) = d and

         A5: x in V and

         A6: V in ( sigma L);

        V is open by A6, Th24;

        then ( inf V) << x by A5, Th26;

        hence thesis by A4;

      end;

       ex_sup_of (VV,L) & ex_sup_of (( waybelow x),L) by YELLOW_0: 17;

      then

       A7: ( "\/" (VV,L)) <= ( sup ( waybelow x)) by A3, YELLOW_0: 34;

      x = ( "\/" (VV,L)) by A1;

      hence thesis by A7, A2, ORDERS_2: 2;

    end;

    theorem :: WAYBEL14:39

    

     Th39: (for x holds ex B be Basis of x st for Y st Y in B holds Y is open filtered) iff for V holds ex VV st V = ( sup VV) & for W st W in VV holds W is co-prime

    proof

      set IPs = ( InclPoset the topology of L);

      

       A1: ( sigma L) = the topology of L by Th23;

      then

       A2: the carrier of IPs = ( sigma L) by YELLOW_1: 1;

      hereby

        assume

         A3: for x be Element of L holds ex X be Basis of x st for Y be Subset of L st Y in X holds Y is open filtered;

        let V be Element of ( InclPoset ( sigma L));

        set X = { Y where Y be Subset of L : Y c= V & ex x be Element of L, bas be Basis of x st x in V & Y in bas & for Yx be Subset of L st Yx in bas holds Yx is open filtered };

        now

          let YY be object;

          assume YY in X;

          then

          consider Y be Subset of L such that

           A4: Y = YY and Y c= V and

           A5: ex x be Element of L, bas be Basis of x st x in V & Y in bas & for Yx be Subset of L st Yx in bas holds Yx is open filtered;

          Y is open by A5;

          then Y in ( sigma L) by Th24;

          hence YY in the carrier of ( InclPoset ( sigma L)) by A4, YELLOW_1: 1;

        end;

        then

        reconsider X as Subset of ( InclPoset ( sigma L)) by TARSKI:def 3;

        take X;

        V in ( sigma L) by A1, A2;

        then

        reconsider Vl = V as Subset of L;

        

         A6: Vl is open by A1, A2, Th24;

        now

          let x be object;

          hereby

            assume

             A7: x in V;

            Vl = V;

            then

            reconsider d = x as Element of L by A7;

            consider bas be Basis of d such that

             A8: for Y be Subset of L st Y in bas holds Y is open filtered by A3;

            consider Y be Subset of L such that

             A9: Y in bas and

             A10: Y c= V by A6, A7, YELLOW_8: 13;

            

             A11: x in Y by A9, YELLOW_8: 12;

            Y in X by A7, A8, A9, A10;

            hence x in ( union X) by A11, TARSKI:def 4;

          end;

          assume x in ( union X);

          then

          consider YY be set such that

           A12: x in YY and

           A13: YY in X by TARSKI:def 4;

          ex Y be Subset of L st Y = YY & Y c= V & ex x be Element of L, bas be Basis of x st x in V & Y in bas & for Yx be Subset of L st Yx in bas holds Yx is open filtered by A13;

          hence x in V by A12;

        end;

        then V = ( union X) by TARSKI: 2;

        hence V = ( sup X) by A1, YELLOW_1: 22;

        let Yp be Element of ( InclPoset ( sigma L));

        assume Yp in X;

        then

        consider Y be Subset of L such that

         A14: Y = Yp and Y c= V and

         A15: ex x be Element of L, bas be Basis of x st x in V & Y in bas & for Yx be Subset of L st Yx in bas holds Yx is open filtered;

        

         A16: Y is open filtered by A15;

        then Y is upper by WAYBEL11:def 4;

        hence Yp is co-prime by A14, A16, Th27;

      end;

      assume

       A17: for V be Element of ( InclPoset ( sigma L)) holds ex X be Subset of ( InclPoset ( sigma L)) st V = ( sup X) & for x be Element of ( InclPoset ( sigma L)) st x in X holds x is co-prime;

      let x be Element of L;

      set bas = { V where V be Element of ( InclPoset ( sigma L)) : x in V & V is co-prime };

      bas c= ( bool the carrier of L)

      proof

        let VV be object;

        assume VV in bas;

        then ex V be Element of ( InclPoset ( sigma L)) st VV = V & x in V & V is co-prime;

        then VV in ( sigma L) by A1, A2;

        hence thesis;

      end;

      then

      reconsider bas as Subset-Family of L;

      reconsider bas as Subset-Family of L;

      bas is Basis of x

      proof

        

         A18: bas is open

        proof

          let VV be Subset of L;

          assume VV in bas;

          then ex V be Element of ( InclPoset ( sigma L)) st VV = V & x in V & V is co-prime;

          hence thesis by A1, A2, PRE_TOPC:def 2;

        end;

        bas is x -quasi_basis

        proof

          now

            per cases ;

              suppose bas is empty;

              then ( Intersect bas) = the carrier of L by SETFAM_1:def 9;

              hence x in ( Intersect bas);

            end;

              suppose

               A19: bas is non empty;

               A20:

              now

                let Y be set;

                assume Y in bas;

                then ex V be Element of ( InclPoset ( sigma L)) st Y = V & x in V & V is co-prime;

                hence x in Y;

              end;

              ( Intersect bas) = ( meet bas) by A19, SETFAM_1:def 9;

              hence x in ( Intersect bas) by A19, A20, SETFAM_1:def 1;

            end;

          end;

          hence x in ( Intersect bas);

          let S be Subset of L;

          assume that

           A21: S is open and

           A22: x in S;

          reconsider S9 = S as Element of IPs by A2, A21, Th24;

          consider X be Subset of IPs such that

           A23: S9 = ( sup X) and

           A24: for x be Element of IPs st x in X holds x is co-prime by A1, A17;

          S9 = ( union X) by A23, YELLOW_1: 22;

          then

          consider V be set such that

           A25: x in V and

           A26: V in X by A22, TARSKI:def 4;

          V in ( sigma L) by A2, A26;

          then

          reconsider V as Subset of L;

          reconsider Vp = V as Element of IPs by A26;

          take V;

          Vp is co-prime by A24, A26;

          hence V in bas by A1, A25;

          ( sup X) is_>=_than X by YELLOW_0: 32;

          then Vp <= ( sup X) by A26, LATTICE3:def 9;

          hence thesis by A23, YELLOW_1: 3;

        end;

        hence thesis by A18;

      end;

      then

      reconsider bas as Basis of x;

      take bas;

      let V be Subset of L;

      assume V in bas;

      then ex Vp be Element of ( InclPoset ( sigma L)) st V = Vp & x in Vp & Vp is co-prime;

      hence thesis by A1, A2, Th24, Th27;

    end;

    theorem :: WAYBEL14:40

    (for V holds ex VV st V = ( sup VV) & for W st W in VV holds W is co-prime) & ( InclPoset ( sigma L)) is continuous iff ( InclPoset ( sigma L)) is completely-distributive

    proof

      ( InclPoset ( sigma L)) = ( InclPoset the topology of L) by Th23;

      hence thesis by WAYBEL_6: 38;

    end;

    theorem :: WAYBEL14:41

    ( InclPoset ( sigma L)) is completely-distributive iff ( InclPoset ( sigma L)) is continuous & (( InclPoset ( sigma L)) opp ) is continuous

    proof

      ( InclPoset ( sigma L)) = ( InclPoset the topology of L) by Th23;

      hence thesis by WAYBEL_6: 39;

    end;

    theorem :: WAYBEL14:42

    L is algebraic implies ex B be Basis of L st B = { ( uparrow x) : x in the carrier of ( CompactSublatt L) }

    proof

      set P = { ( uparrow k) where k be Element of L : k in the carrier of ( CompactSublatt L) };

      P c= ( bool the carrier of L)

      proof

        let x be object;

        assume x in P;

        then ex k be Element of L st x = ( uparrow k) & k in the carrier of ( CompactSublatt L);

        hence thesis;

      end;

      then

      reconsider P as Subset-Family of L;

      reconsider P as Subset-Family of L;

      

       A1: P c= the topology of L

      proof

        let x be object;

        assume x in P;

        then

        consider k be Element of L such that

         A2: x = ( uparrow k) and

         A3: k in the carrier of ( CompactSublatt L);

        k is compact by A3, WAYBEL_8:def 1;

        then ( uparrow k) is Open by WAYBEL_8: 2;

        then ( uparrow k) is open by WAYBEL11: 41;

        hence thesis by A2, PRE_TOPC:def 2;

      end;

      assume

       A4: L is algebraic;

      now

        let x be Point of L;

        set B = { ( uparrow k) where k be Element of L : ( uparrow k) in P & x in ( uparrow k) };

        B c= ( bool the carrier of L)

        proof

          let y be object;

          assume y in B;

          then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in P & x in ( uparrow k);

          hence thesis;

        end;

        then

        reconsider B as Subset-Family of L;

        reconsider B as Subset-Family of L;

        B is Basis of x

        proof

          

           A5: B is open

          proof

            let y be Subset of L;

            assume y in B;

            then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in P & x in ( uparrow k);

            hence thesis by A1, PRE_TOPC:def 2;

          end;

          B is x -quasi_basis

          proof

            now

              per cases ;

                suppose B is empty;

                then ( Intersect B) = the carrier of L by SETFAM_1:def 9;

                hence x in ( Intersect B);

              end;

                suppose

                 A6: B is non empty;

                 A7:

                now

                  let Y be set;

                  assume Y in B;

                  then ex k be Element of L st Y = ( uparrow k) & ( uparrow k) in P & x in ( uparrow k);

                  hence x in Y;

                end;

                ( Intersect B) = ( meet B) by A6, SETFAM_1:def 9;

                hence x in ( Intersect B) by A6, A7, SETFAM_1:def 1;

              end;

            end;

            hence x in ( Intersect B);

            reconsider x9 = x as Element of L;

            let S be Subset of L such that

             A8: S is open and

             A9: x in S;

            

             A10: x = ( sup ( compactbelow x9)) by A4, WAYBEL_8:def 3;

            S is inaccessible by A8, WAYBEL11:def 4;

            then ( compactbelow x9) meets S by A9, A10, WAYBEL11:def 1;

            then

            consider k be object such that

             A11: k in ( compactbelow x9) and

             A12: k in S by XBOOLE_0: 3;

            reconsider k as Element of L by A11;

            

             A13: ( compactbelow x9) = (( downarrow x9) /\ the carrier of ( CompactSublatt L)) by WAYBEL_8: 5;

            then k in ( downarrow x9) by A11, XBOOLE_0:def 4;

            then k <= x9 by WAYBEL_0: 17;

            then

             A14: x in ( uparrow k) by WAYBEL_0: 18;

            take V = ( uparrow k);

            k in the carrier of ( CompactSublatt L) by A11, A13, XBOOLE_0:def 4;

            then ( uparrow k) in P;

            hence V in B by A14;

            S is upper by A8, WAYBEL11:def 4;

            hence thesis by A12, WAYBEL11: 42;

          end;

          hence thesis by A5;

        end;

        then

        reconsider B as Basis of x;

        take B;

        thus B c= P

        proof

          let y be object;

          assume y in B;

          then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in P & x in ( uparrow k);

          hence thesis;

        end;

      end;

      then P is Basis of L by A1, YELLOW_8: 14;

      hence thesis;

    end;

    theorem :: WAYBEL14:43

    (ex B be Basis of L st B = { ( uparrow x) : x in the carrier of ( CompactSublatt L) }) implies ( InclPoset ( sigma L)) is algebraic & for V holds ex VV st V = ( sup VV) & for W st W in VV holds W is co-prime

    proof

      given B be Basis of L such that

       A1: B = { ( uparrow k) where k be Element of L : k in the carrier of ( CompactSublatt L) };

      set IPs = ( InclPoset ( sigma L));

      set IPt = ( InclPoset the topology of L);

      

       A2: the carrier of IPs = ( sigma L) by YELLOW_1: 1;

      

       A3: ( sigma L) = the topology of L by Th23;

      

       A4: IPs = IPt by Th23;

      thus ( InclPoset ( sigma L)) is algebraic

      proof

        thus for X be Element of IPs holds ( compactbelow X) is non empty directed by A3;

        thus IPs is up-complete by A4;

        let X be Element of IPs;

        set cX = ( compactbelow X);

        set GB = { G where G be Subset of L : G in B & G c= X };

        X in ( sigma L) by A2;

        then

        reconsider X9 = X as Subset of L;

        X9 is open by A2, Th24;

        then

         A5: X = ( union GB) by YELLOW_8: 9;

         A6:

        now

          let x be object;

          hereby

            assume x in X;

            then

            consider GG be set such that

             A7: x in GG and

             A8: GG in GB by A5, TARSKI:def 4;

            consider G be Subset of L such that

             A9: G = GG and

             A10: G in B and

             A11: G c= X by A8;

            consider k be Element of L such that

             A12: G = ( uparrow k) and

             A13: k in the carrier of ( CompactSublatt L) by A1, A10;

            k is compact by A13, WAYBEL_8:def 1;

            then ( uparrow k) is Open by WAYBEL_8: 2;

            then ( uparrow k) is open by WAYBEL11: 41;

            then

            reconsider G as Element of IPs by A3, A2, A12, PRE_TOPC:def 2;

            for X be Subset of L st X is open holds X is upper by WAYBEL11:def 4;

            then ( uparrow k) is compact by Th22;

            then

             A14: G is compact by A3, A12, WAYBEL_3: 36;

            G <= X by A11, YELLOW_1: 3;

            then G in cX by A14;

            hence x in ( union cX) by A7, A9, TARSKI:def 4;

          end;

          assume x in ( union cX);

          then

          consider G be set such that

           A15: x in G and

           A16: G in cX by TARSKI:def 4;

          reconsider G as Element of IPs by A16;

          G <= X by A16, WAYBEL_8: 4;

          then G c= X by YELLOW_1: 3;

          hence x in X by A15;

        end;

        ( sup cX) = ( union cX) by A3, YELLOW_1: 22;

        hence thesis by A6, TARSKI: 2;

      end;

      let V be Element of ( InclPoset ( sigma L));

      V in ( sigma L) by A2;

      then

      reconsider V9 = V as Subset of L;

      set GB = { G where G be Subset of L : G in B & G c= V };

      GB c= the carrier of IPs

      proof

        let x be object;

        assume x in GB;

        then

        consider G be Subset of L such that

         A17: G = x and

         A18: G in B and G c= V;

        G is open by A18, YELLOW_8: 10;

        hence thesis by A2, A17, Th24;

      end;

      then

      reconsider GB as Subset of ( InclPoset ( sigma L));

      take GB;

      V9 is open by A2, Th24;

      then V = ( union GB) by YELLOW_8: 9;

      hence V = ( sup GB) by A3, YELLOW_1: 22;

      let x be Element of ( InclPoset ( sigma L));

      assume x in GB;

      then

      consider G be Subset of L such that

       A19: G = x and

       A20: G in B and G c= V;

      ex k be Element of L st G = ( uparrow k) & k in the carrier of ( CompactSublatt L) by A1, A20;

      hence thesis by A19, Th27;

    end;

    theorem :: WAYBEL14:44

    ( InclPoset ( sigma L)) is algebraic & (for V holds ex VV st V = ( sup VV) & for W st W in VV holds W is co-prime) implies ex B be Basis of L st B = { ( uparrow x) : x in the carrier of ( CompactSublatt L) }

    proof

      set IPt = ( InclPoset the topology of L);

      set IPs = ( InclPoset ( sigma L));

      

       A1: the carrier of IPs = ( sigma L) by YELLOW_1: 1;

      set B = { ( uparrow k) where k be Element of L : k in the carrier of ( CompactSublatt L) };

      B c= ( bool the carrier of L)

      proof

        let x be object;

        assume x in B;

        then ex k be Element of L st x = ( uparrow k) & k in the carrier of ( CompactSublatt L);

        hence thesis;

      end;

      then

      reconsider B as Subset-Family of L;

      assume that

       A2: ( InclPoset ( sigma L)) is algebraic and

       A3: for V be Element of ( InclPoset ( sigma L)) holds ex X be Subset of ( InclPoset ( sigma L)) st V = ( sup X) & for x be Element of ( InclPoset ( sigma L)) st x in X holds x is co-prime;

      IPs = IPt by Th23;

      then

      reconsider ips = ( InclPoset ( sigma L)) as algebraic LATTICE by A2;

      reconsider B as Subset-Family of L;

      

       A4: B c= the topology of L

      proof

        let x be object;

        assume x in B;

        then

        consider k be Element of L such that

         A5: x = ( uparrow k) and

         A6: k in the carrier of ( CompactSublatt L);

        k is compact by A6, WAYBEL_8:def 1;

        then ( uparrow k) is Open by WAYBEL_8: 2;

        then ( uparrow k) is open by WAYBEL11: 41;

        hence thesis by A5, PRE_TOPC:def 2;

      end;

      

       A7: ( sigma L) = the topology of L by Th23;

      ips is continuous & for x be Element of L holds ex X be Basis of x st for Y be Subset of L st Y in X holds Y is open filtered by A3, Th39;

      then for x be Element of L holds x = ( "\/" ({ ( inf V) where V be Subset of L : x in V & V in ( sigma L) },L)) by Th37;

      then

       A8: L is continuous by Th38;

      now

        let x be Point of L;

        set Bx = { ( uparrow k) where k be Element of L : ( uparrow k) in B & x in ( uparrow k) };

        Bx c= ( bool the carrier of L)

        proof

          let y be object;

          assume y in Bx;

          then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in B & x in ( uparrow k);

          hence thesis;

        end;

        then

        reconsider Bx as Subset-Family of L;

        reconsider Bx as Subset-Family of L;

        Bx is Basis of x

        proof

          

           A9: Bx is open

          proof

            let y be Subset of L;

            assume y in Bx;

            then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in B & x in ( uparrow k);

            hence thesis by A4, PRE_TOPC:def 2;

          end;

          Bx is x -quasi_basis

          proof

            now

              per cases ;

                suppose Bx is empty;

                then ( Intersect Bx) = the carrier of L by SETFAM_1:def 9;

                hence x in ( Intersect Bx);

              end;

                suppose

                 A10: Bx is non empty;

                 A11:

                now

                  let Y be set;

                  assume Y in Bx;

                  then ex k be Element of L st Y = ( uparrow k) & ( uparrow k) in B & x in ( uparrow k);

                  hence x in Y;

                end;

                ( Intersect Bx) = ( meet Bx) by A10, SETFAM_1:def 9;

                hence x in ( Intersect Bx) by A10, A11, SETFAM_1:def 1;

              end;

            end;

            hence x in ( Intersect Bx);

            let S be Subset of L such that

             A12: S is open and

             A13: x in S;

            reconsider S9 = S as Element of IPt by A7, A1, A12, PRE_TOPC:def 2;

            S9 = ( sup ( compactbelow S9)) by A2, A7, WAYBEL_8:def 3;

            then S9 = ( union ( compactbelow S9)) by YELLOW_1: 22;

            then

            consider UA be set such that

             A14: x in UA and

             A15: UA in ( compactbelow S9) by A13, TARSKI:def 4;

            reconsider UA as Element of IPt by A15;

            UA is compact by A15, WAYBEL_8: 4;

            then

             A16: UA << UA;

            UA in the topology of L by A7, A1;

            then

            reconsider UA9 = UA as Subset of L;

            UA <= S9 by A15, WAYBEL_8: 4;

            then

             A17: UA c= S by YELLOW_1: 3;

            consider F be Subset of ( InclPoset ( sigma L)) such that

             A18: UA = ( sup F) and

             A19: for x be Element of ( InclPoset ( sigma L)) st x in F holds x is co-prime by A3, A7;

            reconsider F9 = F as Subset-Family of L by A1, XBOOLE_1: 1;

            

             A20: UA = ( union F) by A7, A18, YELLOW_1: 22;

            F9 is open by A7, A1, PRE_TOPC:def 2;

            then

            consider G be finite Subset of F9 such that

             A21: UA c= ( union G) by A20, A16, WAYBEL_3: 34;

            ( union G) c= ( union F) by ZFMISC_1: 77;

            then

             A22: UA = ( union G) by A20, A21;

            reconsider G as finite Subset-Family of L by XBOOLE_1: 1;

            consider Gg be finite Subset-Family of L such that

             A23: Gg c= G and

             A24: ( union Gg) = ( union G) and

             A25: for g be Subset of L st g in Gg holds not g c= ( union (Gg \ {g})) by Th1;

            consider U1 be set such that

             A26: x in U1 and

             A27: U1 in Gg by A14, A21, A24, TARSKI:def 4;

            

             A28: Gg c= F by A23, XBOOLE_1: 1;

            then U1 in F by A27;

            then

            reconsider U1 as Element of IPs;

            U1 in the topology of L by A7, A1;

            then

            reconsider U19 = U1 as Subset of L;

            set k = ( inf U19);

            

             A29: U19 c= ( uparrow k)

            proof

              let x be object;

              assume

               A30: x in U19;

              then

              reconsider x9 = x as Element of L;

              k is_<=_than U19 by YELLOW_0: 33;

              then k <= x9 by A30, LATTICE3:def 8;

              hence thesis by WAYBEL_0: 18;

            end;

            U1 is co-prime by A19, A27, A28;

            then

             A31: U19 is filtered upper by Th27;

            now

              set D = { (( downarrow u) ` ) where u be Element of L : u in U19 };

              

               A32: D c= the topology of L

              proof

                let d be object;

                assume d in D;

                then

                consider u be Element of L such that

                 A33: d = (( downarrow u) ` ) and u in U19;

                (( downarrow u) ` ) is open by WAYBEL11: 12;

                hence thesis by A33, PRE_TOPC:def 2;

              end;

              consider u be set such that

               A34: u in U19 by A26;

              reconsider u as Element of L by A34;

              (( downarrow u) ` ) in D by A34;

              then

              reconsider D as non empty Subset of IPt by A32, YELLOW_1: 1;

              assume

               A35: not k in U19;

              now

                assume not UA c= ( union D);

                then

                consider l be object such that

                 A36: l in UA9 and

                 A37: not l in ( union D);

                reconsider l as Element of L by A36;

                consider Uk be set such that

                 A38: l in Uk and

                 A39: Uk in Gg by A21, A24, A36, TARSKI:def 4;

                

                 A40: Gg c= F by A23, XBOOLE_1: 1;

                then Uk in F by A39;

                then

                reconsider Uk as Element of IPs;

                Uk in the topology of L by A7, A1;

                then

                reconsider Uk9 = Uk as Subset of L;

                Uk is co-prime by A19, A39, A40;

                then

                 A41: Uk9 is filtered upper by Th27;

                now

                  assume not l is_<=_than U19;

                  then

                  consider m be Element of L such that

                   A42: m in U19 and

                   A43: not l <= m by LATTICE3:def 8;

                  (( downarrow m) ` ) in D by A42;

                  then not l in (( downarrow m) ` ) by A37, TARSKI:def 4;

                  then l in ( downarrow m) by XBOOLE_0:def 5;

                  hence contradiction by A43, WAYBEL_0: 17;

                end;

                then l <= k by YELLOW_0: 33;

                then

                 A44: k in Uk9 by A38, A41;

                

                 A45: k is_<=_than U19 by YELLOW_0: 33;

                

                 A46: U19 c= Uk

                proof

                  let u be object;

                  assume

                   A47: u in U19;

                  then

                  reconsider d = u as Element of L;

                  k <= d by A45, A47, LATTICE3:def 8;

                  hence thesis by A41, A44;

                end;

                U19 c= ( union (Gg \ {U19}))

                proof

                  let u be object;

                  assume

                   A48: u in U19;

                  Uk in (Gg \ {U19}) by A35, A39, A44, ZFMISC_1: 56;

                  hence thesis by A46, A48, TARSKI:def 4;

                end;

                hence contradiction by A25, A27;

              end;

              then UA c= ( sup D) by YELLOW_1: 22;

              then

               A49: UA <= ( sup D) by YELLOW_1: 3;

              D is directed by A7, A31, Th25;

              then

              consider d be Element of IPt such that

               A50: d in D and

               A51: UA <= d by A16, A49;

              consider u be Element of L such that

               A52: d = (( downarrow u) ` ) and

               A53: u in U19 by A50;

              U1 c= UA by A20, A27, A28, ZFMISC_1: 74;

              then

               A54: u in UA by A53;

              

               A55: u <= u;

              UA c= d by A51, YELLOW_1: 3;

              then not u in ( downarrow u) by A52, A54, XBOOLE_0:def 5;

              hence contradiction by A55, WAYBEL_0: 17;

            end;

            then ( uparrow k) c= U19 by A31, WAYBEL11: 42;

            then

             A56: U19 = ( uparrow k) by A29;

            take V = ( uparrow k);

            U19 is open by A7, A1, PRE_TOPC:def 2;

            then U19 is Open by A8, A31, WAYBEL11: 46;

            then k is compact by A56, WAYBEL_8: 2;

            then k in the carrier of ( CompactSublatt L) by WAYBEL_8:def 1;

            then ( uparrow k) in B;

            hence V in Bx by A26, A29;

            U1 c= UA by A22, A24, A27, ZFMISC_1: 74;

            hence thesis by A56, A17;

          end;

          hence thesis by A9;

        end;

        then

        reconsider Bx as Basis of x;

        take Bx;

        thus Bx c= B

        proof

          let y be object;

          assume y in Bx;

          then ex k be Element of L st y = ( uparrow k) & ( uparrow k) in B & x in ( uparrow k);

          hence thesis;

        end;

      end;

      then

      reconsider B as Basis of L by A4, YELLOW_8: 14;

      take B;

      thus thesis;

    end;

    theorem :: WAYBEL14:45

    (ex B be Basis of L st B = { ( uparrow x) : x in the carrier of ( CompactSublatt L) }) implies L is algebraic

    proof

      given B be Basis of L such that

       A1: B = { ( uparrow k) where k be Element of L : k in the carrier of ( CompactSublatt L) };

      thus for x be Element of L holds ( compactbelow x) is non empty directed;

      thus L is up-complete;

      let x be Element of L;

      set y = ( sup ( compactbelow x));

      set cx = ( compactbelow x);

      set dx = ( downarrow x);

      set dy = ( downarrow y);

      now

        for z be Element of L st z in dx holds z <= x by WAYBEL_0: 17;

        then x is_>=_than dx by LATTICE3:def 9;

        then

         A2: ( sup dx) <= x by YELLOW_0: 32;

        set GB = { G where G be Subset of L : G in B & G c= (dy ` ) };

        

         A3: cx = (dx /\ the carrier of ( CompactSublatt L)) by WAYBEL_8: 5;

        

         A4: y is_>=_than cx by YELLOW_0: 32;

         ex_sup_of (cx,L) & ex_sup_of (dx,L) by YELLOW_0: 17;

        then ( sup ( compactbelow x)) <= ( sup dx) by A3, XBOOLE_1: 17, YELLOW_0: 34;

        then

         A5: y <= x by A2, ORDERS_2: 3;

        assume

         A6: y <> x;

        now

          assume x in dy;

          then x <= y by WAYBEL_0: 17;

          hence contradiction by A6, A5, ORDERS_2: 2;

        end;

        then

         A7: x in (dy ` ) by XBOOLE_0:def 5;

        (dy ` ) = ( union GB) by WAYBEL11: 12, YELLOW_8: 9;

        then

        consider X be set such that

         A8: x in X and

         A9: X in GB by A7, TARSKI:def 4;

        consider G be Subset of L such that

         A10: G = X and

         A11: G in B and

         A12: G c= (dy ` ) by A9;

        consider k be Element of L such that

         A13: G = ( uparrow k) and

         A14: k in the carrier of ( CompactSublatt L) by A1, A11;

        

         A15: k is compact by A14, WAYBEL_8:def 1;

        k <= x by A8, A10, A13, WAYBEL_0: 18;

        then k in cx by A15;

        then k <= y by A4, LATTICE3:def 9;

        then y in ( uparrow k) by WAYBEL_0: 18;

        then y <= y & not y in dy by A12, A13, XBOOLE_0:def 5;

        hence contradiction by WAYBEL_0: 17;

      end;

      hence thesis;

    end;