waybel30.miz



    begin

    theorem :: WAYBEL30:1

    

     Th1: for x be set, D be non empty set holds (x /\ ( union D)) = ( union the set of all (x /\ d) where d be Element of D)

    proof

      let x be set, D be non empty set;

      hereby

        let a be object;

        assume

         A1: a in (x /\ ( union D));

        then a in ( union D) by XBOOLE_0:def 4;

        then

        consider Z be set such that

         A2: a in Z and

         A3: Z in D by TARSKI:def 4;

        

         A4: (x /\ Z) in the set of all (x /\ d) where d be Element of D by A3;

        a in x by A1, XBOOLE_0:def 4;

        then a in (x /\ Z) by A2, XBOOLE_0:def 4;

        hence a in ( union the set of all (x /\ d) where d be Element of D) by A4, TARSKI:def 4;

      end;

      let a be object;

      assume a in ( union the set of all (x /\ d) where d be Element of D);

      then

      consider Z be set such that

       A5: a in Z and

       A6: Z in the set of all (x /\ d) where d be Element of D by TARSKI:def 4;

      consider d be Element of D such that

       A7: Z = (x /\ d) and not contradiction by A6;

      a in d by A5, A7, XBOOLE_0:def 4;

      then

       A8: a in ( union D) by TARSKI:def 4;

      a in x by A5, A7, XBOOLE_0:def 4;

      hence thesis by A8, XBOOLE_0:def 4;

    end;

    theorem :: WAYBEL30:2

    

     Th2: for R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R)) holds ( union D) is Ideal of R

    proof

      let R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R));

      set d = the Element of D;

      D c= the carrier of ( InclPoset ( Ids R));

      then

       A1: D c= ( Ids R) by YELLOW_1: 1;

      

       A2: D c= ( bool the carrier of R)

      proof

        let d be object;

        assume d in D;

        then d in ( Ids R) by A1;

        then ex I be Ideal of R st d = I;

        hence thesis;

      end;

      d in ( Ids R) by A1;

      then

      consider I be Ideal of R such that

       A3: d = I and not contradiction;

      

       A4: for X be Subset of R st X in D holds X is directed

      proof

        let X be Subset of R;

        assume X in D;

        then X in ( Ids R) by A1;

        then ex I be Ideal of R st X = I;

        hence thesis;

      end;

      

       A5: for X,Y be Subset of R st X in D & Y in D holds ex Z be Subset of R st Z in D & (X \/ Y) c= Z

      proof

        let X,Y be Subset of R;

        assume that

         A6: X in D and

         A7: Y in D;

        reconsider X1 = X, Y1 = Y as Element of ( InclPoset ( Ids R)) by A6, A7;

        consider Z1 be Element of ( InclPoset ( Ids R)) such that

         A8: Z1 in D and

         A9: X1 <= Z1 and

         A10: Y1 <= Z1 by A6, A7, WAYBEL_0:def 1;

        Z1 in ( Ids R) by A1, A8;

        then ex I be Ideal of R st Z1 = I;

        then

        reconsider Z = Z1 as Subset of R;

        take Z;

        thus Z in D by A8;

        

         A11: Y1 c= Z1 by A10, YELLOW_1: 3;

        X1 c= Z1 by A9, YELLOW_1: 3;

        hence thesis by A11, XBOOLE_1: 8;

      end;

      

       A12: for X be Subset of R st X in D holds X is lower

      proof

        let X be Subset of R;

        assume X in D;

        then X in ( Ids R) by A1;

        then ex I be Ideal of R st X = I;

        hence thesis;

      end;

      set i = the Element of I;

      i in d by A3;

      hence thesis by A12, A2, A4, A5, TARSKI:def 4, WAYBEL_0: 26, WAYBEL_0: 46;

    end;

     Lm1:

    now

      let R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R)), UD be Element of ( InclPoset ( Ids R)) such that

       A1: UD = ( union D);

      thus D is_<=_than UD

      proof

        let d be Element of ( InclPoset ( Ids R));

        assume

         A2: d in D;

        d c= UD by A1, A2, TARSKI:def 4;

        hence d <= UD by YELLOW_1: 3;

      end;

    end;

     Lm2:

    now

      let R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R)), UD be Element of ( InclPoset ( Ids R)) such that

       A1: UD = ( union D);

      thus for b be Element of ( InclPoset ( Ids R)) st b is_>=_than D holds UD <= b

      proof

        let b be Element of ( InclPoset ( Ids R)) such that

         A2: for a be Element of ( InclPoset ( Ids R)) st a in D holds b >= a;

        UD c= b

        proof

          let x be object;

          assume x in UD;

          then

          consider Z be set such that

           A3: x in Z and

           A4: Z in D by A1, TARSKI:def 4;

          reconsider Z as Element of ( InclPoset ( Ids R)) by A4;

          b >= Z by A2, A4;

          then Z c= b by YELLOW_1: 3;

          hence thesis by A3;

        end;

        hence thesis by YELLOW_1: 3;

      end;

    end;

    registration

      let R be non empty reflexive transitive RelStr;

      cluster ( InclPoset ( Ids R)) -> up-complete;

      coherence

      proof

        set I = ( InclPoset ( Ids R));

        let D be non empty directed Subset of I;

        reconsider UD = ( union D) as Ideal of R by Th2;

        UD in ( Ids R);

        then

        reconsider UD as Element of I by YELLOW_1: 1;

        take UD;

        thus thesis by Lm1, Lm2;

      end;

    end

    theorem :: WAYBEL30:3

    

     Th3: for R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R)) holds ( sup D) = ( union D)

    proof

      let R be non empty reflexive transitive RelStr, D be non empty directed Subset of ( InclPoset ( Ids R));

      reconsider UD = ( union D) as Ideal of R by Th2;

      

       A1: ex_sup_of (D,( InclPoset ( Ids R))) by WAYBEL_0: 75;

      UD in ( Ids R);

      then

      reconsider UD as Element of ( InclPoset ( Ids R)) by YELLOW_1: 1;

      

       A2: for b be Element of ( InclPoset ( Ids R)) st b is_>=_than D holds UD <= b by Lm2;

      D is_<=_than UD by Lm1;

      hence thesis by A2, A1, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL30:4

    

     Th4: for R be Semilattice, D be non empty directed Subset of ( InclPoset ( Ids R)), x be Element of ( InclPoset ( Ids R)) holds ( sup ( {x} "/\" D)) = ( union the set of all (x /\ d) where d be Element of D)

    proof

      let R be Semilattice, D be non empty directed Subset of ( InclPoset ( Ids R)), x be Element of ( InclPoset ( Ids R));

      set I = ( InclPoset ( Ids R)), A = the set of all (x /\ d) where d be Element of D;

      set xD = { (x "/\" d) where d be Element of I : d in D };

      xD c= the carrier of I

      proof

        let a be object;

        assume a in xD;

        then ex d be Element of I st a = (x "/\" d) & d in D;

        hence thesis;

      end;

      then

      reconsider xD as Subset of I;

      

       A1: ex_sup_of (( {x} "/\" D),I) by WAYBEL_2: 1;

      then ex_sup_of (xD,I) by YELLOW_4: 42;

      then

       A2: ( sup xD) is_>=_than xD by YELLOW_0:def 9;

      hereby

        set A = the set of all (x /\ w) where w be Element of D;

        let a be object;

         ex_sup_of (D,I) by WAYBEL_0: 75;

        then ( sup ( {x} "/\" D)) <= (x "/\" ( sup D)) by A1, YELLOW_4: 53;

        then

         A3: ( sup ( {x} "/\" D)) c= (x "/\" ( sup D)) by YELLOW_1: 3;

        assume a in ( sup ( {x} "/\" D));

        then a in (x "/\" ( sup D)) by A3;

        then

         A4: a in (x /\ ( sup D)) by YELLOW_2: 43;

        then a in ( sup D) by XBOOLE_0:def 4;

        then a in ( union D) by Th3;

        then

        consider d be set such that

         A5: a in d and

         A6: d in D by TARSKI:def 4;

        reconsider d as Element of I by A6;

        

         A7: (x /\ d) in A by A6;

        a in x by A4, XBOOLE_0:def 4;

        then a in (x /\ d) by A5, XBOOLE_0:def 4;

        hence a in ( union A) by A7, TARSKI:def 4;

      end;

      let a be object;

      assume a in ( union A);

      then

      consider Z be set such that

       A8: a in Z and

       A9: Z in A by TARSKI:def 4;

      consider d be Element of D such that

       A10: Z = (x /\ d) and not contradiction by A9;

      reconsider d as Element of I;

      

       A11: xD = ( {x} "/\" D) by YELLOW_4: 42;

      then (x "/\" d) in ( {x} "/\" D);

      then ( sup xD) >= (x "/\" d) by A2, A11;

      then

       A12: (x "/\" d) c= ( sup xD) by YELLOW_1: 3;

      (x /\ d) = (x "/\" d) by YELLOW_2: 43;

      then a in ( sup xD) by A12, A8, A10;

      hence thesis by YELLOW_4: 42;

    end;

    registration

      let R be Semilattice;

      cluster ( InclPoset ( Ids R)) -> satisfying_MC;

      coherence

      proof

        set I = ( InclPoset ( Ids R));

        let x be Element of I, D be non empty directed Subset of I;

        

        thus (x "/\" ( sup D)) = (x /\ ( sup D)) by YELLOW_2: 43

        .= (x /\ ( union D)) by Th3

        .= ( union the set of all (x /\ d) where d be Element of D) by Th1

        .= ( sup ( {x} "/\" D)) by Th4;

      end;

    end

    registration

      let R be 1 -element RelStr;

      cluster -> trivial for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of T = the RelStr of R by YELLOW_9:def 4;

        hence thesis;

      end;

    end

    theorem :: WAYBEL30:5

    for S be Scott complete TopLattice, T be complete LATTICE, A be Scott TopAugmentation of T st the RelStr of S = the RelStr of T holds the TopRelStr of A = the TopRelStr of S

    proof

      let S be Scott complete TopLattice, T be complete LATTICE, A be Scott TopAugmentation of T such that

       A1: the RelStr of S = the RelStr of T;

      

       A2: the topology of S = ( sigma S) by WAYBEL14: 23

      .= ( sigma T) by A1, YELLOW_9: 52

      .= the topology of A by YELLOW_9: 51;

       the RelStr of A = the RelStr of S by A1, YELLOW_9:def 4;

      hence thesis by A2;

    end;

    theorem :: WAYBEL30:6

    for N be Lawson complete TopLattice, T be complete LATTICE, A be Lawson correct TopAugmentation of T st the RelStr of N = the RelStr of T holds the TopRelStr of A = the TopRelStr of N

    proof

      let N be Lawson complete TopLattice, T be complete LATTICE, A be Lawson correct TopAugmentation of T such that

       A1: the RelStr of N = the RelStr of T;

      

       A2: ( omega T) = ( omega N) by A1, WAYBEL19: 3;

      set S = the Scott correct TopAugmentation of T;

      set l = the lower correct TopAugmentation of T;

      

       A3: the RelStr of l = the RelStr of T by YELLOW_9:def 4;

      

       A4: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      (the topology of S \/ the topology of l) c= ( bool the carrier of N)

      proof

        let a be object;

        assume a in (the topology of S \/ the topology of l);

        then a in the topology of S or a in the topology of l by XBOOLE_0:def 3;

        hence thesis by A1, A4, A3;

      end;

      then

      reconsider X = (the topology of S \/ the topology of l) as Subset-Family of N;

      reconsider X as Subset-Family of N;

      

       A5: the topology of l = ( omega T) by WAYBEL19:def 2;

      (( sigma N) \/ ( omega N)) is prebasis of N by WAYBEL19:def 3;

      then

       A6: (( sigma T) \/ ( omega N)) is prebasis of N by A1, YELLOW_9: 52;

      

       A7: the topology of S = ( sigma T) by YELLOW_9: 51;

      the carrier of N = (the carrier of S \/ the carrier of l) by A1, A4, A3;

      then N is Refinement of S, l by A2, A6, A5, A7, YELLOW_9:def 6;

      

      then

       A8: the topology of N = ( UniCl ( FinMeetCl X)) by YELLOW_9: 56

      .= ( lambda T) by A1, A5, A7, WAYBEL19: 33

      .= the topology of A by WAYBEL19:def 4;

       the RelStr of A = the RelStr of N by A1, YELLOW_9:def 4;

      hence thesis by A8;

    end;

    theorem :: WAYBEL30:7

    for N be Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for A be Subset of N, J be Subset of S st A = J & J is closed holds A is closed

    proof

      let N be Lawson complete TopLattice, S be Scott TopAugmentation of N, A be Subset of N, J be Subset of S such that

       A1: A = J;

      assume J is closed;

      then

       A2: (( [#] S) \ J) is open;

      

       A3: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then N is Lawson correct TopAugmentation of S by YELLOW_9:def 4;

      hence (( [#] N) \ A) is open by A1, A3, A2, WAYBEL19: 37;

    end;

    registration

      let A be complete LATTICE;

      cluster ( lambda A) -> non empty;

      coherence

      proof

        set S = the Lawson correct TopAugmentation of A;

        ( InclPoset the topology of S) is non trivial;

        hence thesis by WAYBEL19:def 4;

      end;

    end

    registration

      let S be Scott complete TopLattice;

      cluster ( InclPoset ( sigma S)) -> complete non trivial;

      coherence ;

    end

    registration

      let N be Lawson complete TopLattice;

      cluster ( InclPoset ( sigma N)) -> complete non trivial;

      coherence ;

      cluster ( InclPoset ( lambda N)) -> complete non trivial;

      coherence

      proof

        set S = the Lawson correct TopAugmentation of N;

        ( InclPoset the topology of S) is complete non trivial;

        hence thesis by WAYBEL19:def 4;

      end;

    end

    theorem :: WAYBEL30:8

    

     Th8: for T be non empty reflexive RelStr holds ( sigma T) c= { (W \ ( uparrow F)) where W,F be Subset of T : W in ( sigma T) & F is finite }

    proof

      let T be non empty reflexive RelStr;

      let s be object;

      reconsider ss = s as set by TARSKI: 1;

      

       A1: (ss \ ( uparrow ( {} T))) = s;

      assume s in ( sigma T);

      hence thesis by A1;

    end;

    theorem :: WAYBEL30:9

    

     Th9: for N be Lawson complete TopLattice holds ( lambda N) = the topology of N

    proof

      let N be Lawson complete TopLattice;

      N is Lawson correct TopAugmentation of N by YELLOW_9: 44;

      hence thesis by WAYBEL19:def 4;

    end;

    theorem :: WAYBEL30:10

    

     Th10: for N be Lawson complete TopLattice holds ( sigma N) c= ( lambda N)

    proof

      let N be Lawson complete TopLattice;

      set Z = { (W \ ( uparrow F)) where W,F be Subset of N : W in ( sigma N) & F is finite };

      Z is Basis of N by WAYBEL19: 32;

      then Z c= the topology of N by TOPS_2: 64;

      then

       A1: Z c= ( lambda N) by Th9;

      ( sigma N) c= Z by Th8;

      hence thesis by A1;

    end;

    theorem :: WAYBEL30:11

    for M,N be complete LATTICE st the RelStr of M = the RelStr of N holds ( lambda M) = ( lambda N)

    proof

      let M,N be complete LATTICE such that

       A1: the RelStr of M = the RelStr of N;

      

       A2: ( lambda N) = ( UniCl ( FinMeetCl (( sigma N) \/ ( omega N)))) by WAYBEL19: 33;

      

       A3: ( lambda M) = ( UniCl ( FinMeetCl (( sigma M) \/ ( omega M)))) by WAYBEL19: 33;

      ( sigma M) = ( sigma N) by A1, YELLOW_9: 52;

      hence thesis by A1, A3, A2, WAYBEL19: 3;

    end;

    theorem :: WAYBEL30:12

    

     Th12: for N be Lawson complete TopLattice, X be Subset of N holds X in ( lambda N) iff X is open by Th9;

    registration

      cluster TopSpace-like -> Scott for reflexive1 -element TopRelStr;

      coherence by TDLAT_3: 15;

    end

    registration

      cluster trivial -> Lawson for complete TopLattice;

      coherence

      proof

        let T be complete TopLattice;

        assume T is trivial;

        then the carrier of T is 1 -element;

        then

        reconsider W = T as 1 -element complete TopLattice by STRUCT_0:def 19;

        set N = the Lawson correct TopAugmentation of W;

        

         A1: the RelStr of T = the RelStr of N by YELLOW_9:def 4;

        the topology of W = { {} , the carrier of W} by TDLAT_3:def 2;

        

        then the topology of T = the topology of N by A1, TDLAT_3:def 2

        .= ( lambda T) by WAYBEL19:def 4

        .= ( UniCl ( FinMeetCl (( sigma T) \/ ( omega T)))) by WAYBEL19: 33;

        then ( FinMeetCl (( omega T) \/ ( sigma T))) is Basis of T by YELLOW_9: 22;

        hence (( omega T) \/ ( sigma T)) is prebasis of T by YELLOW_9: 23;

      end;

    end

    registration

      cluster strict continuous lower-bounded meet-continuous Scott for complete TopLattice;

      existence

      proof

        set A = the strict1 -element TopLattice;

        take A;

        thus thesis;

      end;

    end

    registration

      cluster strict continuous compact Hausdorff Lawson for complete TopLattice;

      existence

      proof

        set R = the strict trivial complete TopLattice;

        take R;

        thus thesis;

      end;

    end

    scheme :: WAYBEL30:sch1

    EmptySch { A() -> Scott TopLattice , X() -> set , F( set) -> set } :

{ F(w) where w be Element of A() : w in {} } = {} ;

      thus { F(w) where w be Element of A() : w in {} } c= {}

      proof

        let a be object;

        assume a in { F(w) where w be Element of A() : w in {} };

        then

         A1: ex w be Element of A() st a = F(w) & w in {} ;

        assume not a in {} ;

        thus thesis by A1;

      end;

      thus thesis;

    end;

    theorem :: WAYBEL30:13

    

     Th13: for N be meet-continuous LATTICE, A be Subset of N st A is property(S) holds ( uparrow A) is property(S)

    proof

      let N be meet-continuous LATTICE, A be Subset of N such that

       A1: for D be non empty directed Subset of N st ( sup D) in A holds ex y be Element of N st y in D & for x be Element of N st x in D & x >= y holds x in A;

      let D be non empty directed Subset of N;

      assume ( sup D) in ( uparrow A);

      then

      consider a be Element of N such that

       A2: a <= ( sup D) and

       A3: a in A by WAYBEL_0:def 16;

      reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0: 5;

      a = ( sup ( {a} "/\" D)) by A2, WAYBEL_2: 52;

      then

      consider y be Element of N such that

       A4: y in (aa "/\" D) and

       A5: for x be Element of N st x in (aa "/\" D) & x >= y holds x in A by A1, A3;

      (aa "/\" D) = { (a "/\" d) where d be Element of N : d in D } by YELLOW_4: 42;

      then

      consider d be Element of N such that

       A6: y = (a "/\" d) and

       A7: d in D by A4;

      take d;

      thus d in D by A7;

      let x be Element of N such that x in D and

       A8: x >= d;

      d >= y by A6, YELLOW_0: 23;

      then

       A9: x >= y by A8, ORDERS_2: 3;

      y in A by A4, A5, ORDERS_2: 1;

      hence thesis by A9, WAYBEL_0:def 16;

    end;

    registration

      let N be meet-continuous LATTICE, A be property(S) Subset of N;

      cluster ( uparrow A) -> property(S);

      coherence by Th13;

    end

    theorem :: WAYBEL30:14

    

     Th14: for N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, A be Subset of N st A in ( lambda N) holds ( uparrow A) in ( sigma S)

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, A be Subset of N;

      assume A in ( lambda N);

      then

       A1: A is open by Th12;

      

       A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider Y = A as Subset of S;

      

       A3: S is meet-continuous by A2, YELLOW12: 14;

      reconsider UA = ( uparrow A) as Subset of S by A2;

      

       A4: ( uparrow A) = ( uparrow Y) by A2, WAYBEL_0: 13;

      Y is property(S) by A1, A2, WAYBEL19: 36, YELLOW12: 19;

      then UA is open by A3, A4, WAYBEL11: 15;

      then ( uparrow A) in the topology of S;

      hence thesis by WAYBEL14: 23;

    end;

    theorem :: WAYBEL30:15

    

     Th15: for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for A be Subset of N, J be Subset of S st A = J holds A is open implies ( uparrow J) is open

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, A be Subset of N, J be Subset of S such that

       A1: A = J;

      assume A is open;

      then A in ( lambda N) by Th12;

      then

       A2: ( uparrow A) in ( sigma S) by Th14;

       the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then ( uparrow J) in ( sigma S) by A2, A1, WAYBEL_0: 13;

      hence thesis by WAYBEL14: 24;

    end;

    theorem :: WAYBEL30:16

    

     Th16: for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for x be Point of S, y be Point of N holds for J be Basis of y st x = y holds { ( uparrow A) where A be Subset of N : A in J } is Basis of x

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, x be Point of S, y be Point of N, J be Basis of y such that

       A1: x = y;

      set Z = { ( uparrow A) where A be Subset of N : A in J };

      set K = Z;

      

       A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      K c= ( bool the carrier of S)

      proof

        let k be object;

        assume k in K;

        then ex A be Subset of N st k = ( uparrow A) & A in J;

        hence thesis by A2;

      end;

      then

      reconsider K as Subset-Family of S;

      K is Basis of x

      proof

        

         A3: K is open

        proof

          let k be Subset of S;

          assume k in K;

          then

          consider A be Subset of N such that

           A4: k = ( uparrow A) and

           A5: A in J;

          reconsider A9 = A as Subset of S by A2;

          ( uparrow A9) is open by A5, Th15, YELLOW_8: 12;

          then ( uparrow A9) in the topology of S;

          then ( uparrow A) in the topology of S by A2, WAYBEL_0: 13;

          hence thesis by A4;

        end;

        K is x -quasi_basis

        proof

          for k be set st k in K holds x in k

          proof

            let k be set;

            assume k in K;

            then

            consider A be Subset of N such that

             A6: k = ( uparrow A) and

             A7: A in J;

            

             A8: A c= ( uparrow A) by WAYBEL_0: 16;

            y in ( Intersect J) by YELLOW_8:def 1;

            then y in A by A7, SETFAM_1: 43;

            hence thesis by A8, A1, A6;

          end;

          hence x in ( Intersect K) by SETFAM_1: 43;

          let sA be Subset of S such that

           A9: sA is open and

           A10: x in sA;

          sA is upper by A9, WAYBEL11:def 4;

          then

           A11: ( uparrow sA) c= sA by WAYBEL_0: 24;

          reconsider lA = sA as Subset of N by A2;

          N is Lawson correct TopAugmentation of S by A2, YELLOW_9:def 4;

          then lA is open by A9, WAYBEL19: 37;

          then lA in ( lambda N) by Th12;

          then

           A12: ( uparrow lA) in ( sigma S) by Th14;

          

           A13: lA c= ( uparrow lA) by WAYBEL_0: 16;

          ( sigma N) c= ( lambda N) by Th10;

          then ( sigma S) c= ( lambda N) by A2, YELLOW_9: 52;

          then ( uparrow lA) is open by A12, Th12;

          then

          consider lV1 be Subset of N such that

           A14: lV1 in J and

           A15: lV1 c= ( uparrow lA) by A13, A1, A10, YELLOW_8:def 1;

          reconsider sUV = ( uparrow lV1) as Subset of S by A2;

          take sUV;

          thus sUV in K by A14;

          

           A16: lV1 is_coarser_than ( uparrow lA) by A15, WAYBEL12: 16;

          sA c= ( uparrow sA) by WAYBEL_0: 16;

          then

           A17: sA = ( uparrow sA) by A11;

          ( uparrow sA) = ( uparrow lA) by A2, WAYBEL_0: 13;

          hence thesis by A16, A17, YELLOW12: 28;

        end;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL30:17

    

     Th17: for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for X be upper Subset of N, Y be Subset of S st X = Y holds ( Int X) = ( Int Y)

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, X be upper Subset of N, Y be Subset of S such that

       A1: X = Y;

      

       A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider K = ( uparrow ( Int X)) as Subset of S;

      reconsider sX = ( Int X) as Subset of S by A2;

      

       A3: K c= Y

      proof

        let a be object;

        

         A4: ( Int X) c= X by TOPS_1: 16;

        assume

         A5: a in K;

        then

        reconsider x = a as Element of N;

        

         A6: X c= ( uparrow X) by WAYBEL_0: 16;

        ( uparrow X) c= X by WAYBEL_0: 24;

        then

         A7: ( uparrow X) = X by A6;

        ex y be Element of N st y <= x & y in ( Int X) by A5, WAYBEL_0:def 16;

        hence thesis by A7, A1, A4, WAYBEL_0:def 16;

      end;

      

       A8: ( Int X) c= ( uparrow ( Int X)) by WAYBEL_0: 16;

      ( uparrow sX) is open by Th15;

      then K is open by A2, WAYBEL_0: 13;

      then ( uparrow ( Int X)) c= ( Int Y) by A3, TOPS_1: 24;

      hence ( Int X) c= ( Int Y) by A8;

      reconsider A = ( Int Y) as Subset of N by A2;

      N is Lawson correct TopAugmentation of S by A2, YELLOW_9:def 4;

      then A is open by WAYBEL19: 37;

      hence thesis by A1, TOPS_1: 16, TOPS_1: 24;

    end;

    theorem :: WAYBEL30:18

    for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for X be lower Subset of N, Y be Subset of S st X = Y holds ( Cl X) = ( Cl Y)

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, X be lower Subset of N, Y be Subset of S such that

       A1: X = Y;

      

       A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider A = ( Cl Y) as Subset of N;

      (( Cl X) ` ) = (( Cl ((X ` ) ` )) ` )

      .= ( Int (X ` )) by TOPS_1:def 1

      .= ( Int (Y ` )) by A1, A2, Th17

      .= (( Cl ((Y ` ) ` )) ` ) by TOPS_1:def 1

      .= (A ` ) by A2;

      hence thesis by TOPS_1: 1;

    end;

    theorem :: WAYBEL30:19

    

     Th19: for M,N be complete LATTICE, LM be Lawson correct TopAugmentation of M, LN be Lawson correct TopAugmentation of N st ( InclPoset ( sigma N)) is continuous holds the topology of [:LM, LN qua TopSpace:] = ( lambda [:M, N:])

    proof

      let M,N be complete LATTICE, LM be Lawson correct TopAugmentation of M, LN be Lawson correct TopAugmentation of N such that

       A1: ( InclPoset ( sigma N)) is continuous;

      set SMN = the non empty Scott correct TopAugmentation of [:M, N:];

      set lMN = the non empty lower correct TopAugmentation of [:M, N:];

      set LMN = the non empty Lawson correct TopAugmentation of [:M, N:];

      

       A2: [:LM, LN qua TopSpace:] = the TopStruct of LMN

      proof

        set lN = the non empty lower correct TopAugmentation of N;

        set lM = the non empty lower correct TopAugmentation of M;

        set SN = the non empty Scott correct TopAugmentation of N;

        set SM = the non empty Scott correct TopAugmentation of M;

        

         A3: LN is Refinement of SN, lN by WAYBEL19: 29;

        

         A4: the RelStr of lN = the RelStr of N by YELLOW_9:def 4;

        (( omega LMN) \/ ( sigma LMN)) is prebasis of LMN by WAYBEL19:def 3;

        then

         A5: (( omega LMN) \/ ( sigma LMN)) is prebasis of the TopStruct of LMN by YELLOW12: 33;

        

         A6: the RelStr of LM = the RelStr of M by YELLOW_9:def 4;

        

         A7: the RelStr of LN = the RelStr of N by YELLOW_9:def 4;

        

         A8: the RelStr of LMN = the RelStr of [:M, N:] by YELLOW_9:def 4;

        

         A9: the carrier of [:LM, LN qua TopSpace:] = [:the carrier of LM, the carrier of LN:] by BORSUK_1:def 2

        .= the carrier of LMN by A6, A7, A8, YELLOW_3:def 2;

        

         A10: the topology of [:lM, lN qua TopSpace:] = ( omega [:M, N:]) by WAYBEL19: 15

        .= ( omega LMN) by A8, WAYBEL19: 3;

        

         A11: the RelStr of SN = the RelStr of N by YELLOW_9:def 4;

         the RelStr of SM = the RelStr of M by YELLOW_9:def 4

        .= the RelStr of ( Sigma M) by YELLOW_9:def 4;

        then

         A12: the TopStruct of SM = the TopStruct of ( Sigma M) by WAYBEL29: 13;

        

         A13: the RelStr of lM = the RelStr of M by YELLOW_9:def 4;

         the RelStr of SN = the RelStr of N by YELLOW_9:def 4

        .= the RelStr of ( Sigma N) by YELLOW_9:def 4;

        then the TopStruct of SN = the TopStruct of ( Sigma N) by WAYBEL29: 13;

        

        then

         A14: the topology of [:SM, SN qua TopSpace:] = the topology of [:( Sigma M), ( Sigma N) qua TopSpace:] by A12, WAYBEL29: 7

        .= ( sigma [:M, N:]) by A1, WAYBEL29: 30

        .= ( sigma LMN) by A8, YELLOW_9: 52;

        

         A15: the RelStr of SM = the RelStr of M by YELLOW_9:def 4;

        

         A16: LM is Refinement of SM, lM by WAYBEL19: 29;

        then [:LM, LN qua TopSpace:] is Refinement of [:SM, SN qua TopSpace:], [:lM, lN qua TopSpace:] by A3, A15, A11, A13, A4, YELLOW12: 50;

        then the carrier of the TopStruct of LMN = (the carrier of [:SM, SN qua TopSpace:] \/ the carrier of [:lM, lN qua TopSpace:]) by A9, YELLOW_9:def 6;

        then the TopStruct of LMN is Refinement of [:SM, SN qua TopSpace:], [:lM, lN qua TopSpace:] by A5, A14, A10, YELLOW_9:def 6;

        hence thesis by A16, A3, A15, A11, A13, A4, A9, YELLOW12: 49;

      end;

      LMN is Refinement of SMN, lMN by WAYBEL19: 29;

      then

      reconsider R = [:LM, LN qua TopSpace:] as Refinement of SMN, lMN by A2, YELLOW12: 47;

      the topology of [:LM, LN qua TopSpace:] = the topology of R;

      hence thesis by WAYBEL19: 34;

    end;

    theorem :: WAYBEL30:20

    

     Th20: for M,N be complete LATTICE, P be Lawson correct TopAugmentation of [:M, N:], Q be Lawson correct TopAugmentation of M, R be Lawson correct TopAugmentation of N st ( InclPoset ( sigma N)) is continuous holds the TopStruct of P = [:Q, R qua TopSpace:]

    proof

      let M,N be complete LATTICE, P be Lawson correct TopAugmentation of [:M, N:], Q be Lawson correct TopAugmentation of M, R be Lawson correct TopAugmentation of N such that

       A1: ( InclPoset ( sigma N)) is continuous;

      

       A2: the topology of P = ( lambda [:M, N:]) by WAYBEL19:def 4

      .= the topology of [:Q, R qua TopSpace:] by A1, Th19;

      

       A3: the RelStr of Q = the RelStr of M by YELLOW_9:def 4;

      

       A4: the RelStr of R = the RelStr of N by YELLOW_9:def 4;

       the RelStr of P = the RelStr of [:M, N:] by YELLOW_9:def 4;

      

      then the carrier of P = [:the carrier of Q, the carrier of N:] by A3, YELLOW_3:def 2

      .= the carrier of [:Q, R qua TopSpace:] by A4, BORSUK_1:def 2;

      hence thesis by A2;

    end;

    theorem :: WAYBEL30:21

    

     Th21: for N be meet-continuous Lawson complete TopLattice, x be Element of N holds (x "/\" ) is continuous

    proof

      let N be meet-continuous Lawson complete TopLattice, x be Element of N;

      for X be non empty Subset of N holds (x "/\" ) preserves_inf_of X by YELLOW13: 11;

      hence thesis by WAYBEL21: 45;

    end;

    registration

      let N be meet-continuous Lawson complete TopLattice, x be Element of N;

      cluster (x "/\" ) -> continuous;

      coherence by Th21;

    end

    theorem :: WAYBEL30:22

    

     Th22: for N be meet-continuous Lawson complete TopLattice st ( InclPoset ( sigma N)) is continuous holds N is topological_semilattice

    proof

      let N be meet-continuous Lawson complete TopLattice such that

       A1: ( InclPoset ( sigma N)) is continuous;

      set NN = the Lawson correct TopAugmentation of [:N, N:];

      N is TopAugmentation of N by YELLOW_9: 44;

      then

       A2: the TopStruct of NN = [:N, N qua TopSpace:] by A1, Th20;

      

       A3: the RelStr of NN = the RelStr of [:N, N:] by YELLOW_9:def 4;

      then

      reconsider h = ( inf_op N) as Function of NN, N;

      

       A4: the RelStr of N = the RelStr of N;

      

       A5: h is directed-sups-preserving

      proof

        let X be Subset of NN;

        assume X is non empty directed;

        then

        reconsider X1 = X as non empty directed Subset of [:N, N:] by A3, WAYBEL_0: 3;

        ( inf_op N) preserves_sup_of X1 by WAYBEL_0:def 37;

        hence thesis by A3, A4, WAYBEL_0: 65;

      end;

      

       A6: h is infs-preserving by A3, WAYBEL_0:def 32, A4, WAYBEL_0: 65;

      then h is SemilatticeHomomorphism of NN, N by WAYBEL21: 5;

      then

       A7: h is continuous by A5, A6, WAYBEL21: 46;

      

       A8: the TopStruct of N = the TopStruct of N;

      let g be Function of [:N, N qua TopSpace:], N;

      assume g = ( inf_op N);

      hence thesis by A2, A7, A8, YELLOW12: 36;

    end;

     Lm3:

    now

      let S,T,x1,x2 be set such that

       A1: x1 in S and

       A2: x2 in T;

      

       A3: ( dom <:( pr2 (S,T)), ( pr1 (S,T)):>) = (( dom ( pr2 (S,T))) /\ ( dom ( pr1 (S,T)))) by FUNCT_3:def 7

      .= (( dom ( pr2 (S,T))) /\ [:S, T:]) by FUNCT_3:def 4

      .= ( [:S, T:] /\ [:S, T:]) by FUNCT_3:def 5

      .= [:S, T:];

       [x1, x2] in [:S, T:] by A1, A2, ZFMISC_1: 87;

      

      hence ( <:( pr2 (S,T)), ( pr1 (S,T)):> . [x1, x2]) = [(( pr2 (S,T)) . (x1,x2)), (( pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def 7

      .= [x2, (( pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def 5

      .= [x2, x1] by A1, A2, FUNCT_3:def 4;

    end;

    theorem :: WAYBEL30:23

    for N be meet-continuous Lawson complete TopLattice st ( InclPoset ( sigma N)) is continuous holds N is Hausdorff iff for X be Subset of [:N, N qua TopSpace:] st X = the InternalRel of N holds X is closed

    proof

      let N be meet-continuous Lawson complete TopLattice such that

       A1: ( InclPoset ( sigma N)) is continuous;

      

       A2: [:the carrier of N, the carrier of N:] = the carrier of [:N, N qua TopSpace:] by BORSUK_1:def 2;

      hereby

        reconsider D = ( id the carrier of N) as Subset of [:N, N qua TopSpace:] by BORSUK_1:def 2;

        set INF = ( inf_op N), f = <:( pr1 (the carrier of N,the carrier of N)), INF:>;

        assume N is Hausdorff;

        then

         A3: D is closed by YELLOW12: 46;

        

         A4: the carrier of [:N, N:] = [:the carrier of N, the carrier of N:] by YELLOW_3:def 2;

        then

        reconsider f as Function of [:N, N qua TopSpace:], [:N, N qua TopSpace:] by A2, FUNCT_3: 58;

        let X be Subset of [:N, N qua TopSpace:] such that

         A5: X = the InternalRel of N;

        

         A6: for x,y be Element of N holds (f . [x, y]) = [x, (x "/\" y)]

        proof

          let x,y be Element of N;

          

           A7: ( dom ( pr1 (the carrier of N,the carrier of N))) = [:the carrier of N, the carrier of N:] by FUNCT_2:def 1;

          

           A8: [x, y] in [:the carrier of N, the carrier of N:] by ZFMISC_1: 87;

          ( dom INF) = [:the carrier of N, the carrier of N:] by A4, FUNCT_2:def 1;

          

          hence (f . [x, y]) = [(( pr1 (the carrier of N,the carrier of N)) . (x,y)), (INF . (x,y))] by A8, A7, FUNCT_3: 49

          .= [x, (INF . (x,y))] by FUNCT_3:def 4

          .= [x, (x "/\" y)] by WAYBEL_2:def 4;

        end;

        

         A9: X = (f " D)

        proof

          hereby

            let a be object;

            assume

             A10: a in X;

            then

            consider s,t be object such that

             A11: s in the carrier of N and

             A12: t in the carrier of N and

             A13: a = [s, t] by A5, ZFMISC_1:def 2;

            reconsider s, t as Element of N by A11, A12;

            s <= t by A5, A10, A13, ORDERS_2:def 5;

            then (s "/\" t) = s by YELLOW_0: 25;

            then (f . [s, t]) = [s, s] by A6;

            then

             A14: (f . a) in D by A13, RELAT_1:def 10;

            ( dom f) = the carrier of [:N, N qua TopSpace:] by FUNCT_2:def 1;

            then a in ( dom f) by A2, A11, A12, A13, ZFMISC_1: 87;

            hence a in (f " D) by A14, FUNCT_1:def 7;

          end;

          let a be object;

          assume

           A15: a in (f " D);

          then

           A16: (f . a) in D by FUNCT_1:def 7;

          consider s,t be object such that

           A17: s in the carrier of N and

           A18: t in the carrier of N and

           A19: a = [s, t] by A2, A15, ZFMISC_1:def 2;

          reconsider s, t as Element of N by A17, A18;

          (f . a) = [s, (s "/\" t)] by A6, A19;

          then s = (s "/\" t) by A16, RELAT_1:def 10;

          then s <= t by YELLOW_0: 25;

          hence thesis by A5, A19, ORDERS_2:def 5;

        end;

        reconsider INF as Function of [:N, N qua TopSpace:], N by A2, A4;

        N is topological_semilattice by A1, Th22;

        then

         A20: INF is continuous;

        ( pr1 (the carrier of N,the carrier of N)) is continuous Function of [:N, N qua TopSpace:], N by YELLOW12: 39;

        then f is continuous by A20, YELLOW12: 41;

        hence X is closed by A9, A3;

      end;

      assume

       A21: for X be Subset of [:N, N qua TopSpace:] st X = the InternalRel of N holds X is closed;

      

       A22: (the InternalRel of N /\ the InternalRel of (N ~ )) c= ( id the carrier of N) by YELLOW12: 23;

      ( id the carrier of N) c= (the InternalRel of N /\ the InternalRel of (N ~ )) by YELLOW12: 22;

      then

       A23: ( id the carrier of N) = (the InternalRel of N /\ the InternalRel of (N ~ )) by A22;

      for A be Subset of [:N, N qua TopSpace:] st A = ( id the carrier of N) holds A is closed

      proof

        reconsider f = <:( pr2 (the carrier of N,the carrier of N)), ( pr1 (the carrier of N,the carrier of N)):> as continuous Function of [:N, N qua TopSpace:], [:N, N qua TopSpace:] by YELLOW12: 42;

        reconsider X = the InternalRel of N, Y = the InternalRel of (N ~ ) as Subset of [:N, N qua TopSpace:] by BORSUK_1:def 2;

        let A be Subset of [:N, N qua TopSpace:] such that

         A24: A = ( id the carrier of N);

        reconsider X, Y as Subset of [:N, N qua TopSpace:];

        

         A25: X is closed by A21;

        

         A26: ( dom f) = [:the carrier of N, the carrier of N:] by YELLOW12: 4;

        

         A27: (f .: X) = Y

        proof

          thus (f .: X) c= Y

          proof

            let y be object;

            assume y in (f .: X);

            then

            consider x be object such that x in ( dom f) and

             A28: x in X and

             A29: y = (f . x) by FUNCT_1:def 6;

            consider x1,x2 be object such that

             A30: x1 in the carrier of N and

             A31: x2 in the carrier of N and

             A32: x = [x1, x2] by A28, ZFMISC_1:def 2;

            (f . x) = [x2, x1] by A30, A31, A32, Lm3;

            hence thesis by A28, A29, A32, RELAT_1:def 7;

          end;

          let y be object;

          assume

           A33: y in Y;

          then

          consider y1,y2 be object such that

           A34: y1 in the carrier of N and

           A35: y2 in the carrier of N and

           A36: y = [y1, y2] by ZFMISC_1:def 2;

          

           A37: [y2, y1] in X by A33, A36, RELAT_1:def 7;

          (f . [y2, y1]) = y by A34, A35, A36, Lm3;

          hence thesis by A26, A37, FUNCT_1:def 6;

        end;

        f is being_homeomorphism by YELLOW12: 43;

        then Y is closed by A25, A27, TOPS_2: 58;

        hence thesis by A23, A24, A25;

      end;

      hence thesis by YELLOW12: 46;

    end;

    definition

      let N be non empty reflexive RelStr, X be Subset of N;

      :: WAYBEL30:def1

      func X ^0 -> Subset of N equals { u where u be Element of N : for D be non empty directed Subset of N st u <= ( sup D) holds X meets D };

      coherence

      proof

        defpred P[ Element of N] means for D be non empty directed Subset of N st $1 <= ( sup D) holds X meets D;

        thus { u where u be Element of N : P[u] } is Subset of N from DOMAIN_1:sch 7;

      end;

    end

    registration

      let N be non empty reflexive antisymmetric RelStr, X be empty Subset of N;

      cluster (X ^0 ) -> empty;

      coherence

      proof

        (X ^0 ) c= {}

        proof

          let a be object such that

           A1: a in (X ^0 ) and not a in {} ;

          consider u be Element of N such that a = u and

           A2: for D be non empty directed Subset of N st u <= ( sup D) holds X meets D by A1;

          reconsider D = {u} as non empty directed Subset of N by WAYBEL_0: 5;

          

           A3: X misses D;

          u <= ( sup D) by YELLOW_0: 39;

          hence contradiction by A3, A2;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL30:24

    for N be non empty reflexive RelStr, A,J be Subset of N st A c= J holds (A ^0 ) c= (J ^0 )

    proof

      let N be non empty reflexive RelStr, A,J be Subset of N such that

       A1: A c= J;

      let a be object;

      assume a in (A ^0 );

      then

      consider u be Element of N such that

       A2: a = u and

       A3: for D be non empty directed Subset of N st u <= ( sup D) holds A meets D;

      for D be non empty directed Subset of N st u <= ( sup D) holds J meets D by A1, A3, XBOOLE_1: 63;

      hence thesis by A2;

    end;

    theorem :: WAYBEL30:25

    

     Th25: for N be non empty reflexive RelStr, x be Element of N holds (( uparrow x) ^0 ) = ( wayabove x)

    proof

      let N be non empty reflexive RelStr, x be Element of N;

      thus (( uparrow x) ^0 ) c= ( wayabove x)

      proof

        let a be object;

        assume a in (( uparrow x) ^0 );

        then

        consider u be Element of N such that

         A1: a = u and

         A2: for D be non empty directed Subset of N st u <= ( sup D) holds ( uparrow x) meets D;

        u >> x

        proof

          let D be non empty directed Subset of N;

          assume u <= ( sup D);

          then ( uparrow x) meets D by A2;

          then

          consider d be object such that

           A3: d in (( uparrow x) /\ D) by XBOOLE_0: 4;

          reconsider d as Element of N by A3;

          take d;

          thus d in D by A3, XBOOLE_0:def 4;

          d in ( uparrow x) by A3, XBOOLE_0:def 4;

          hence thesis by WAYBEL_0: 18;

        end;

        hence thesis by A1;

      end;

      let a be object;

      assume

       A4: a in ( wayabove x);

      then

      reconsider b = a as Element of N;

      now

        

         A5: b >> x by A4, WAYBEL_3: 8;

        let D be non empty directed Subset of N;

        assume b <= ( sup D);

        then

        consider d be Element of N such that

         A6: d in D and

         A7: x <= d by A5;

        d in ( uparrow x) by A7, WAYBEL_0: 18;

        hence ( uparrow x) meets D by A6, XBOOLE_0: 3;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL30:26

    

     Th26: for N be Scott TopLattice, X be upper Subset of N holds ( Int X) c= (X ^0 )

    proof

      let N be Scott TopLattice, X be upper Subset of N;

      let x be object;

      assume

       A1: x in ( Int X);

      then

      reconsider y = x as Element of N;

      now

        

         A2: ( Int X) is upper inaccessible by WAYBEL11:def 4;

        let D be non empty directed Subset of N;

        assume y <= ( sup D);

        then ( sup D) in ( Int X) by A2, A1;

        then D meets ( Int X) by A2;

        hence X meets D by TOPS_1: 16, XBOOLE_1: 63;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL30:27

    

     Th27: for N be non empty reflexive RelStr, X,Y be Subset of N holds ((X ^0 ) \/ (Y ^0 )) c= ((X \/ Y) ^0 )

    proof

      let N be non empty reflexive RelStr, X,Y be Subset of N;

      let a be object;

      assume

       A1: a in ((X ^0 ) \/ (Y ^0 ));

      then

      reconsider b = a as Element of N;

      now

        let D be non empty directed Subset of N such that

         A2: b <= ( sup D);

        now

          per cases by A1, XBOOLE_0:def 3;

            suppose a in (X ^0 );

            then ex x be Element of N st a = x & for D be non empty directed Subset of N st x <= ( sup D) holds X meets D;

            then X meets D by A2;

            then (X /\ D) <> {} ;

            then ((X /\ D) \/ (Y /\ D)) <> {} ;

            hence ((X \/ Y) /\ D) <> {} by XBOOLE_1: 23;

          end;

            suppose a in (Y ^0 );

            then ex y be Element of N st a = y & for D be non empty directed Subset of N st y <= ( sup D) holds Y meets D;

            then Y meets D by A2;

            then (Y /\ D) <> {} ;

            then ((X /\ D) \/ (Y /\ D)) <> {} ;

            hence ((X \/ Y) /\ D) <> {} by XBOOLE_1: 23;

          end;

        end;

        hence (X \/ Y) meets D;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL30:28

    

     Th28: for N be meet-continuous LATTICE, X,Y be upper Subset of N holds ((X ^0 ) \/ (Y ^0 )) = ((X \/ Y) ^0 )

    proof

      let N be meet-continuous LATTICE, X,Y be upper Subset of N;

      thus ((X ^0 ) \/ (Y ^0 )) c= ((X \/ Y) ^0 ) by Th27;

      assume not ((X \/ Y) ^0 ) c= ((X ^0 ) \/ (Y ^0 ));

      then

      consider s be object such that

       A1: s in ((X \/ Y) ^0 ) and

       A2: not s in ((X ^0 ) \/ (Y ^0 ));

      

       A3: not s in (X ^0 ) by A2, XBOOLE_0:def 3;

      

       A4: not s in (Y ^0 ) by A2, XBOOLE_0:def 3;

      reconsider s as Element of N by A1;

      consider D be non empty directed Subset of N such that

       A5: s <= ( sup D) and

       A6: X misses D by A3;

      consider E be non empty directed Subset of N such that

       A7: s <= ( sup E) and

       A8: Y misses E by A4;

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

      then s <= (( sup D) "/\" ( sup E)) by A5, A7, YELLOW_3: 2;

      then

       A9: s <= ( sup (D "/\" E)) by WAYBEL_2: 51;

      ex xy be Element of N st s = xy & for D be non empty directed Subset of N st xy <= ( sup D) holds (X \/ Y) meets D by A1;

      then (X \/ Y) meets (D "/\" E) by A9;

      then

       A10: ((X \/ Y) /\ (D "/\" E)) <> {} ;

      X misses (D "/\" E) by A6, YELLOW12: 21;

      then

       A11: (X /\ (D "/\" E)) = {} ;

      Y misses (D "/\" E) by A8, YELLOW12: 21;

      then ((X /\ (D "/\" E)) \/ (Y /\ (D "/\" E))) = {} by A11;

      hence contradiction by A10, XBOOLE_1: 23;

    end;

    theorem :: WAYBEL30:29

    

     Th29: for S be meet-continuous Scott TopLattice, F be finite Subset of S holds ( Int ( uparrow F)) c= ( union { ( wayabove x) where x be Element of S : x in F })

    proof

      let S be meet-continuous Scott TopLattice, F be finite Subset of S;

      defpred P[ set] means ex UU be Subset-Family of S st UU = { ( uparrow x) where x be Element of S : x in $1 } & (( union UU) ^0 ) = ( union { (( uparrow x) ^0 ) where x be Element of S : x in $1 });

      

       A1: for b,J be set st b in F & J c= F & P[J] holds P[(J \/ {b})]

      proof

        let b,J be set;

        assume that

         A2: b in F and J c= F;

        reconsider bb = b as Element of S by A2;

        

         A3: (( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) \/ (( uparrow bb) ^0 )) = ( union { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) })

        proof

          { (( uparrow x) ^0 ) where x be Element of S : x in J } c= { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) }

          proof

            let a be object;

            assume a in { (( uparrow x) ^0 ) where x be Element of S : x in J };

            then

             A4: ex y be Element of S st a = (( uparrow y) ^0 ) & y in J;

            J c= (J \/ {b}) by XBOOLE_1: 7;

            hence thesis by A4;

          end;

          then

           A5: ( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) c= ( union { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) }) by ZFMISC_1: 77;

          

           A6: {b} c= (J \/ {b}) by XBOOLE_1: 7;

          b in {b} by TARSKI:def 1;

          then (( uparrow bb) ^0 ) in { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) } by A6;

          then (( uparrow bb) ^0 ) c= ( union { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) }) by ZFMISC_1: 74;

          hence (( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) \/ (( uparrow bb) ^0 )) c= ( union { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) }) by A5, XBOOLE_1: 8;

          let a be object;

          assume a in ( union { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) });

          then

          consider A be set such that

           A7: a in A and

           A8: A in { (( uparrow x) ^0 ) where x be Element of S : x in (J \/ {b}) } by TARSKI:def 4;

          consider y be Element of S such that

           A9: A = (( uparrow y) ^0 ) and

           A10: y in (J \/ {b}) by A8;

          per cases by A10, XBOOLE_0:def 3;

            suppose y in J;

            then (( uparrow y) ^0 ) in { (( uparrow x) ^0 ) where x be Element of S : x in J };

            then

             A11: a in ( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) by A7, A9, TARSKI:def 4;

            ( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) c= (( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) \/ (( uparrow bb) ^0 )) by XBOOLE_1: 7;

            hence thesis by A11;

          end;

            suppose

             A12: y in {b};

            

             A13: (( uparrow bb) ^0 ) c= (( union { (( uparrow x) ^0 ) where x be Element of S : x in J }) \/ (( uparrow bb) ^0 )) by XBOOLE_1: 7;

            y = b by A12, TARSKI:def 1;

            hence thesis by A13, A7, A9;

          end;

        end;

        assume P[J];

        then

        consider UU be Subset-Family of S such that

         A14: UU = { ( uparrow x) where x be Element of S : x in J } and

         A15: (( union UU) ^0 ) = ( union { (( uparrow x) ^0 ) where x be Element of S : x in J });

        reconsider I = (UU \/ {( uparrow bb)}) as Subset-Family of S;

        take I;

        thus I = { ( uparrow x) where x be Element of S : x in (J \/ {b}) }

        proof

          thus I c= { ( uparrow x) where x be Element of S : x in (J \/ {b}) }

          proof

            let a be object such that

             A16: a in I;

            per cases by A16, XBOOLE_0:def 3;

              suppose

               A17: a in UU;

              

               A18: J c= (J \/ {b}) by XBOOLE_1: 7;

              ex x be Element of S st a = ( uparrow x) & x in J by A17, A14;

              hence thesis by A18;

            end;

              suppose

               A19: a in {( uparrow bb)};

              

               A20: b in {b} by TARSKI:def 1;

              

               A21: {b} c= (J \/ {b}) by XBOOLE_1: 7;

              a = ( uparrow bb) by A19, TARSKI:def 1;

              hence thesis by A20, A21;

            end;

          end;

          let a be object;

          assume a in { ( uparrow x) where x be Element of S : x in (J \/ {b}) };

          then

          consider x be Element of S such that

           A22: a = ( uparrow x) and

           A23: x in (J \/ {b});

          per cases by A23, XBOOLE_0:def 3;

            suppose

             A24: x in J;

            

             A25: UU c= (UU \/ {( uparrow bb)}) by XBOOLE_1: 7;

            ( uparrow x) in UU by A24, A14;

            hence thesis by A25, A22;

          end;

            suppose

             A26: x in {b};

            

             A27: {( uparrow bb)} c= (UU \/ {( uparrow bb)}) by XBOOLE_1: 7;

            

             A28: a in {( uparrow x)} by A22, TARSKI:def 1;

            x = b by A26, TARSKI:def 1;

            hence thesis by A27, A28;

          end;

        end;

        

         A29: (( union UU) \/ ( uparrow bb)) = ( union I)

        proof

          thus (( union UU) \/ ( uparrow bb)) c= ( union I)

          proof

            let a be object such that

             A30: a in (( union UU) \/ ( uparrow bb));

            per cases by A30, XBOOLE_0:def 3;

              suppose

               A31: a in ( union UU);

              

               A32: UU c= I by XBOOLE_1: 7;

              ex A be set st a in A & A in UU by A31, TARSKI:def 4;

              hence thesis by A32, TARSKI:def 4;

            end;

              suppose

               A33: a in ( uparrow bb);

              

               A34: ( uparrow bb) in {( uparrow bb)} by TARSKI:def 1;

               {( uparrow bb)} c= (UU \/ {( uparrow bb)}) by XBOOLE_1: 7;

              hence thesis by A34, A33, TARSKI:def 4;

            end;

          end;

          let a be object;

          assume a in ( union I);

          then

          consider A be set such that

           A35: a in A and

           A36: A in I by TARSKI:def 4;

          per cases by A36, XBOOLE_0:def 3;

            suppose A in UU;

            then A c= ( union UU) by ZFMISC_1: 74;

            then

             A37: a in ( union UU) by A35;

            ( union UU) c= (( union UU) \/ ( uparrow bb)) by XBOOLE_1: 7;

            hence thesis by A37;

          end;

            suppose

             A38: A in {( uparrow bb)};

            

             A39: ( uparrow bb) c= (( union UU) \/ ( uparrow bb)) by XBOOLE_1: 7;

            A = ( uparrow bb) by A38, TARSKI:def 1;

            hence thesis by A39, A35;

          end;

        end;

        for X be Subset of S st X in UU holds X is upper

        proof

          let X be Subset of S;

          assume X in UU;

          then ex x be Element of S st X = ( uparrow x) & x in J by A14;

          hence thesis;

        end;

        then ( union UU) is upper by WAYBEL_0: 28;

        hence thesis by A3, A15, A29, Th28;

      end;

      

       A40: P[ {} ]

      proof

        deffunc F( Element of S) = (( uparrow $1) ^0 );

        reconsider UU = {} as Subset-Family of S by XBOOLE_1: 2;

        take UU;

        reconsider K = ( union UU) as empty Subset of S;

        

         A41: (K ^0 ) is empty;

        thus UU = { ( uparrow x) where x be Element of S : x in {} }

        proof

          deffunc F( Element of S) = ( uparrow $1);

          { F(x) where x be Element of S : x in {} } = {} from EmptySch;

          hence thesis;

        end;

        { F(x) where x be Element of S : x in {} } = {} from EmptySch;

        hence thesis by A41;

      end;

      

       A42: { (( uparrow x) ^0 ) where x be Element of S : x in F } = { ( wayabove x) where x be Element of S : x in F }

      proof

        thus { (( uparrow x) ^0 ) where x be Element of S : x in F } c= { ( wayabove x) where x be Element of S : x in F }

        proof

          let a be object;

          assume a in { (( uparrow x) ^0 ) where x be Element of S : x in F };

          then

          consider x be Element of S such that

           A43: a = (( uparrow x) ^0 ) and

           A44: x in F;

          (( uparrow x) ^0 ) = ( wayabove x) by Th25;

          hence thesis by A43, A44;

        end;

        let a be object;

        assume a in { ( wayabove x) where x be Element of S : x in F };

        then

        consider x be Element of S such that

         A45: a = ( wayabove x) and

         A46: x in F;

        (( uparrow x) ^0 ) = ( wayabove x) by Th25;

        hence thesis by A45, A46;

      end;

      

       A47: F is finite;

       P[F] from FINSET_1:sch 2( A47, A40, A1);

      then (( uparrow F) ^0 ) = ( union { ( wayabove x) where x be Element of S : x in F }) by A42, YELLOW_9: 4;

      hence thesis by Th26;

    end;

    theorem :: WAYBEL30:30

    

     Th30: for N be Lawson complete TopLattice holds N is continuous iff N is meet-continuous Hausdorff

    proof

      let N be Lawson complete TopLattice;

      thus N is continuous implies N is meet-continuous Hausdorff;

      assume

       A1: N is meet-continuous Hausdorff;

      thus

       A2: for x be Element of N holds ( waybelow x) is non empty directed;

      thus N is up-complete;

      for x,y be Element of N st not x <= y holds ex u be Element of N st u << x & not u <= y

      proof

        reconsider J = { (O \ ( uparrow F)) where O,F be Subset of N : O in ( sigma N) & F is finite } as Basis of N by WAYBEL19: 32;

        set S = the Scott TopAugmentation of N;

        

         A3: for N be Semilattice, x,y be Element of N st ex u be Element of N st u << x & not u <= (x "/\" y) holds ex u be Element of N st u << x & not u <= y

        proof

          let N be Semilattice, x,y be Element of N;

          given u be Element of N such that

           A4: u << x and

           A5: not u <= (x "/\" y);

          take u;

          thus u << x by A4;

          assume

           A6: u <= y;

          u <= x by A4, WAYBEL_3: 1;

          then (u "/\" u) <= (x "/\" y) by A6, YELLOW_3: 2;

          hence contradiction by A5, YELLOW_0: 25;

        end;

        let x,y be Element of N;

        assume not x <= y;

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

        then

        consider W,V be Subset of N such that

         A7: W is open and

         A8: V is open and

         A9: x in W and

         A10: (x "/\" y) in V and

         A11: W misses V by A1;

        V = ( union { G where G be Subset of N : G in J & G c= V }) by A8, YELLOW_8: 9;

        then

        consider K be set such that

         A12: (x "/\" y) in K and

         A13: K in { G where G be Subset of N : G in J & G c= V } by A10, TARSKI:def 4;

        consider V1 be Subset of N such that

         A14: K = V1 and

         A15: V1 in J and

         A16: V1 c= V by A13;

        consider U2,F be Subset of N such that

         A17: V1 = (U2 \ ( uparrow F)) and

         A18: U2 in ( sigma N) and

         A19: F is finite by A15;

        

         A20: the RelStr of S = the RelStr of N by YELLOW_9:def 4;

        then

        reconsider x1 = x, y1 = y as Element of S;

        

         A21: ex_inf_of ( {x1, y1},S) by YELLOW_0: 21;

        reconsider U1 = U2 as Subset of S by A20;

        reconsider WU1 = (W /\ U2) as Subset of N;

        reconsider W1 = WU1 as Subset of S by A20;

        

         A22: ( uparrow W1) = ( uparrow WU1) by A20, WAYBEL_0: 13;

        U2 in ( sigma S) by A20, A18, YELLOW_9: 52;

        then

         A23: U1 is open by WAYBEL14: 24;

        then

         A24: U1 is upper by WAYBEL11:def 4;

        WU1 c= ( uparrow F)

        proof

          

           A25: W misses V1 by A11, A16, XBOOLE_1: 63;

          

           A26: (WU1 \ ( uparrow F)) c= (U1 \ ( uparrow F)) by XBOOLE_1: 17, XBOOLE_1: 33;

          let w be object;

          assume that

           A27: w in WU1 and

           A28: not w in ( uparrow F);

          

           A29: w in W by A27, XBOOLE_0:def 4;

          w in (WU1 \ ( uparrow F)) by A27, A28, XBOOLE_0:def 5;

          hence contradiction by A26, A17, A29, A25, XBOOLE_0: 3;

        end;

        then WU1 is_coarser_than ( uparrow F) by WAYBEL12: 16;

        then

         A30: ( uparrow WU1) c= ( uparrow F) by YELLOW12: 28;

        

         A31: (x1 "/\" y1) <= x1 by YELLOW_0: 23;

        (x "/\" y) = ( inf {x, y}) by YELLOW_0: 40

        .= ( "/\" ( {x1, y1},S)) by A20, A21, YELLOW_0: 27

        .= (x1 "/\" y1) by YELLOW_0: 40;

        then (x1 "/\" y1) in U1 by A12, A14, A17, XBOOLE_0:def 5;

        then x1 in U1 by A24, A31;

        then

         A32: x in W1 by A9, XBOOLE_0:def 4;

        W1 c= ( uparrow W1) by WAYBEL_0: 16;

        then

         A33: x in ( uparrow W1) by A32;

        reconsider F1 = F as finite Subset of S by A20, A19;

        

         A34: ( uparrow F1) = ( uparrow F) by A20, WAYBEL_0: 13;

        N is Lawson correct TopAugmentation of S by A20, YELLOW_9:def 4;

        then U2 is open by A23, WAYBEL19: 37;

        then ( uparrow W1) c= ( Int ( uparrow F1)) by A7, A1, A30, A22, A34, Th15, TOPS_1: 24;

        then

         A35: x in ( Int ( uparrow F1)) by A33;

        S is meet-continuous by A1, A20, YELLOW12: 14;

        then ( Int ( uparrow F1)) c= ( union { ( wayabove u) where u be Element of S : u in F1 }) by Th29;

        then

        consider A be set such that

         A36: x in A and

         A37: A in { ( wayabove u) where u be Element of S : u in F1 } by A35, TARSKI:def 4;

        consider u be Element of S such that

         A38: A = ( wayabove u) and

         A39: u in F1 by A37;

        reconsider u1 = u as Element of N by A20;

        

         A40: ( wayabove u1) = ( wayabove u) by A20, YELLOW12: 13;

        now

          take u1;

          thus u1 << x by A36, A38, A40, WAYBEL_3: 8;

          ( uparrow u1) c= ( uparrow F) by A39, YELLOW12: 30;

          then not (x "/\" y) in ( uparrow u1) by A12, A14, A17, XBOOLE_0:def 5;

          hence not u1 <= (x "/\" y) by WAYBEL_0: 18;

        end;

        then

        consider u2 be Element of N such that

         A41: u2 << x and

         A42: not u2 <= y by A3;

        take u2;

        thus thesis by A41, A42;

      end;

      hence thesis by A2, WAYBEL_3: 24;

    end;

    registration

      cluster continuous Lawson -> Hausdorff for complete TopLattice;

      coherence ;

      cluster meet-continuous Lawson Hausdorff -> continuous for complete TopLattice;

      coherence by Th30;

    end

    definition

      let N be non empty TopRelStr;

      :: WAYBEL30:def2

      attr N is with_small_semilattices means for x be Point of N holds ex J be basis of x st for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting;

      :: WAYBEL30:def3

      attr N is with_compact_semilattices means for x be Point of N holds ex J be basis of x st for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting & A is compact;

      :: WAYBEL30:def4

      attr N is with_open_semilattices means

      : Def4: for x be Point of N holds ex J be Basis of x st for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting;

    end

    registration

      cluster with_open_semilattices -> with_small_semilattices for non empty TopSpace-like TopRelStr;

      coherence

      proof

        let N be non empty TopSpace-like TopRelStr;

        assume

         A1: for x be Point of N holds ex J be Basis of x st for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting;

        let x be Point of N;

        consider J be Basis of x such that

         A2: for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting by A1;

        reconsider J as basis of x by YELLOW13: 23;

        take J;

        thus thesis by A2;

      end;

      cluster with_compact_semilattices -> with_small_semilattices for non empty TopSpace-like TopRelStr;

      coherence

      proof

        let N be non empty TopSpace-like TopRelStr;

        assume

         A3: for x be Point of N holds ex J be basis of x st for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting & A is compact;

        let x be Point of N;

        consider J be basis of x such that

         A4: for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting & A is compact by A3;

        take J;

        thus thesis by A4;

      end;

      cluster anti-discrete -> with_small_semilattices with_open_semilattices for non empty TopRelStr;

      coherence

      proof

        let T be non empty TopRelStr;

        assume T is anti-discrete;

        then

        reconsider W = T as anti-discrete non empty TopRelStr;

        set J = {the carrier of W};

         A5:

        now

          let A be Subset of W;

          

           A6: ( subrelstr ( [#] W)) is infs-inheriting;

          assume A in J;

          then

          reconsider K = ( subrelstr A) as infs-inheriting SubRelStr of T by A6, TARSKI:def 1;

          K is meet-inheriting;

          hence ( subrelstr A) is meet-inheriting;

        end;

        

         A7: W is with_open_semilattices

        proof

          let x be Point of W;

          reconsider J as Basis of x by YELLOW13: 13;

          take J;

          let A be Subset of W;

          assume A in J;

          hence thesis by A5;

        end;

        W is with_small_semilattices

        proof

          let x be Point of W;

          reconsider J as basis of x by YELLOW13: 21;

          take J;

          let A be Subset of W;

          assume A in J;

          hence thesis by A5;

        end;

        hence thesis by A7;

      end;

      cluster reflexive TopSpace-like -> with_compact_semilattices for 1 -element TopRelStr;

      coherence

      proof

        let T be 1 -element TopRelStr;

        assume T is reflexive TopSpace-like;

        then

        reconsider W = T as reflexive1 -element TopSpace-like TopRelStr;

        W is with_compact_semilattices

        proof

          let x be Point of W;

          reconsider J = {the carrier of W} as basis of x by YELLOW13: 21;

          take J;

          let A be Subset of W;

          assume

           A8: A in J;

          ( subrelstr ( [#] W)) is infs-inheriting;

          then

          reconsider K = ( subrelstr A) as infs-inheriting SubRelStr of T by A8, TARSKI:def 1;

          K is meet-inheriting;

          hence ( subrelstr A) is meet-inheriting;

          A = ( [#] W) by A8, TARSKI:def 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster strict trivial lower for TopLattice;

      existence

      proof

        set T = the strict1 -element TopLattice;

        take T;

        thus thesis;

      end;

    end

    theorem :: WAYBEL30:31

    

     Th31: for N be topological_semilattice with_infima TopPoset, C be Subset of N st ( subrelstr C) is meet-inheriting holds ( subrelstr ( Cl C)) is meet-inheriting

    proof

      let N be topological_semilattice with_infima TopPoset, C be Subset of N such that

       A1: ( subrelstr C) is meet-inheriting;

      set A = ( Cl C), S = ( subrelstr A);

      let x,y be Element of N such that

       A2: x in the carrier of S and

       A3: y in the carrier of S and ex_inf_of ( {x, y},N);

      

       A4: the carrier of S = A by YELLOW_0:def 15;

      for V be a_neighborhood of (x "/\" y) holds V meets C

      proof

        set NN = [:N, N qua TopSpace:];

        let V be a_neighborhood of (x "/\" y);

        

         A5: the carrier of NN = [:the carrier of N, the carrier of N:] by BORSUK_1:def 2;

        then

        reconsider xy = [x, y] as Point of NN by YELLOW_3:def 2;

        the carrier of [:N, N:] = [:the carrier of N, the carrier of N:] by YELLOW_3:def 2;

        then

        reconsider f = ( inf_op N) as Function of NN, N by A5;

        

         A6: (f . xy) = (f . (x,y))

        .= (x "/\" y) by WAYBEL_2:def 4;

        f is continuous by YELLOW13:def 5;

        then

        consider H be a_neighborhood of xy such that

         A7: (f .: H) c= V by A6, BORSUK_1:def 1;

        consider A be Subset-Family of NN such that

         A8: ( Int H) = ( union A) and

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

        xy in ( union A) by A8, CONNSP_2:def 1;

        then

        consider K be set such that

         A10: xy in K and

         A11: K in A by TARSKI:def 4;

        consider Ix,Iy be Subset of N such that

         A12: K = [:Ix, Iy:] and

         A13: Ix is open and

         A14: Iy is open by A9, A11;

        

         A15: x in Ix by A10, A12, ZFMISC_1: 87;

        

         A16: y in Iy by A10, A12, ZFMISC_1: 87;

        

         A17: Ix = ( Int Ix) by A13, TOPS_1: 23;

        Iy = ( Int Iy) by A14, TOPS_1: 23;

        then

        reconsider Iy as a_neighborhood of y by A16, CONNSP_2:def 1;

        Iy meets C by A3, A4, CONNSP_2: 27;

        then

        consider iy be object such that

         A18: iy in Iy and

         A19: iy in C by XBOOLE_0: 3;

        reconsider Ix as a_neighborhood of x by A15, A17, CONNSP_2:def 1;

        Ix meets C by A2, A4, CONNSP_2: 27;

        then

        consider ix be object such that

         A20: ix in Ix and

         A21: ix in C by XBOOLE_0: 3;

        reconsider ix, iy as Element of N by A20, A18;

        now

           [ix, iy] in K by A12, A20, A18, ZFMISC_1: 87;

          then

           A22: [ix, iy] in ( Int H) by A8, A11, TARSKI:def 4;

          take a = (ix "/\" iy);

          

           A23: ( dom f) = the carrier of [:N, N:] by FUNCT_2:def 1;

          

           A24: ( Int H) c= H by TOPS_1: 16;

          (f . (ix,iy)) = (ix "/\" iy) by WAYBEL_2:def 4;

          then (ix "/\" iy) in (f .: H) by A24, A23, A22, FUNCT_1:def 6;

          hence a in V by A7;

          

           A25: ex_inf_of ( {ix, iy},N) by YELLOW_0: 21;

          the carrier of ( subrelstr C) = C by YELLOW_0:def 15;

          then ( inf {ix, iy}) in C by A25, A1, A21, A19;

          hence a in C by YELLOW_0: 40;

        end;

        hence thesis by XBOOLE_0: 3;

      end;

      then (x "/\" y) in ( Cl C) by CONNSP_2: 27;

      hence thesis by A4, YELLOW_0: 40;

    end;

    theorem :: WAYBEL30:32

    

     Th32: for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds (for x be Point of S holds ex J be Basis of x st for W be Subset of S st W in J holds W is Filter of S) iff N is with_open_semilattices

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N;

      

       A1: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      hereby

        assume

         A2: for x be Point of S holds ex J be Basis of x st for W be Subset of S st W in J holds W is Filter of S;

        thus N is with_open_semilattices

        proof

          let x be Point of N;

          defpred P[ set] means ex U1 be Filter of N, F be finite Subset of N, W1 be Subset of N st $1 = W1 & (U1 \ ( uparrow F)) = $1 & x in $1 & W1 is open;

          consider SF be Subset-Family of N such that

           A3: for W be Subset of N holds W in SF iff P[W] from SUBSET_1:sch 3;

          reconsider SF as Subset-Family of N;

           A4:

          now

            reconsider BL = { (O \ ( uparrow F)) where O,F be Subset of N : O in ( sigma N) & F is finite } as Basis of N by WAYBEL19: 32;

            

             A5: BL c= the topology of N by TOPS_2: 64;

            reconsider y = x as Point of S by A1;

            let W be Subset of N such that

             A6: W is open and

             A7: x in W;

            consider By be Basis of y such that

             A8: for A be Subset of S st A in By holds A is Filter of S by A2;

            W = ( union { G where G be Subset of N : G in BL & G c= W }) by A6, YELLOW_8: 9;

            then

            consider K be set such that

             A9: x in K and

             A10: K in { G where G be Subset of N : G in BL & G c= W } by A7, TARSKI:def 4;

            consider G be Subset of N such that

             A11: K = G and

             A12: G in BL and

             A13: G c= W by A10;

            consider V,F be Subset of N such that

             A14: G = (V \ ( uparrow F)) and

             A15: V in ( sigma N) and

             A16: F is finite by A12;

            reconsider F as finite Subset of N by A16;

            

             A17: not x in ( uparrow F) by A9, A11, A14, XBOOLE_0:def 5;

            reconsider V as Subset of S by A1;

            

             A18: y in V by A9, A11, A14, XBOOLE_0:def 5;

            

             A19: ( sigma N) = ( sigma S) by A1, YELLOW_9: 52;

            then V is open by A15, WAYBEL14: 24;

            then

            consider U1 be Subset of S such that

             A20: U1 in By and

             A21: U1 c= V by A18, YELLOW_8: 13;

            reconsider U2 = U1 as Subset of N by A1;

            U1 is Filter of S by A8, A20;

            then

            reconsider U2 as Filter of N by A1, WAYBEL_0: 4, WAYBEL_0: 25;

            (U2 \ ( uparrow F)) is Subset of N;

            then

            reconsider IT = (U1 \ ( uparrow F)) as Subset of N;

            take U2, F, IT;

            thus IT = (U2 \ ( uparrow F));

            y in U1 by A20, YELLOW_8: 12;

            hence x in IT by A17, XBOOLE_0:def 5;

            U1 is open by A20, YELLOW_8: 12;

            then U1 in ( sigma S) by WAYBEL14: 24;

            then IT in BL by A19;

            hence IT is open by A5;

            IT c= G by A14, A21, XBOOLE_1: 33;

            hence IT c= W by A13;

          end;

          SF is Basis of x

          proof

            

             A22: SF is open

            proof

              let a be Subset of N;

              assume

               A23: a in SF;

              reconsider W = a as Subset of N;

              ex U1 be Filter of N, F be finite Subset of N, W1 be Subset of N st W1 = W & (U1 \ ( uparrow F)) = W & x in W & W1 is open by A3, A23;

              hence thesis;

            end;

            SF is x -quasi_basis

            proof

              for a be set st a in SF holds x in a

              proof

                let a be set;

                assume

                 A24: a in SF;

                then

                reconsider W = a as Subset of N;

                ex U1 be Filter of N, F be finite Subset of N, W1 be Subset of N st W1 = W & (U1 \ ( uparrow F)) = W & x in W & W1 is open by A3, A24;

                hence thesis;

              end;

              hence x in ( Intersect SF) by SETFAM_1: 43;

              let W be Subset of N;

              assume that

               A25: W is open and

               A26: x in W;

              consider U2 be Filter of N, F be finite Subset of N, IT be Subset of N such that

               A27: IT = (U2 \ ( uparrow F)) and

               A28: x in IT and

               A29: IT is open and

               A30: IT c= W by A25, A26, A4;

              take IT;

              thus thesis by A3, A27, A28, A29, A30;

            end;

            hence thesis by A22;

          end;

          then

          reconsider SF as Basis of x;

          take SF;

          let W be Subset of N;

          assume W in SF;

          then

          consider U1 be Filter of N, F be finite Subset of N, W1 be Subset of N such that W1 = W and

           A31: (U1 \ ( uparrow F)) = W and x in W and W1 is open by A3;

          set SW = ( subrelstr W);

          thus SW is meet-inheriting

          proof

            let a,b be Element of N such that

             A32: a in the carrier of SW and

             A33: b in the carrier of SW and ex_inf_of ( {a, b},N);

            

             A34: the carrier of SW = W by YELLOW_0:def 15;

            then

             A35: b in U1 by A31, A33, XBOOLE_0:def 5;

            

             A36: not a in ( uparrow F) by A34, A31, A32, XBOOLE_0:def 5;

            for y be Element of N st y <= (a "/\" b) holds not y in F

            proof

              

               A37: (a "/\" b) <= a by YELLOW_0: 23;

              let y be Element of N;

              assume y <= (a "/\" b);

              then y <= a by A37, ORDERS_2: 3;

              hence thesis by A36, WAYBEL_0:def 16;

            end;

            then

             A38: not (a "/\" b) in ( uparrow F) by WAYBEL_0:def 16;

            a in U1 by A34, A31, A32, XBOOLE_0:def 5;

            then

            consider z be Element of N such that

             A39: z in U1 and

             A40: z <= a and

             A41: z <= b by A35, WAYBEL_0:def 2;

            (z "/\" z) <= (a "/\" b) by A40, A41, YELLOW_3: 2;

            then z <= (a "/\" b) by YELLOW_0: 25;

            then (a "/\" b) in U1 by A39, WAYBEL_0:def 20;

            then (a "/\" b) in W by A38, A31, XBOOLE_0:def 5;

            hence thesis by A34, YELLOW_0: 40;

          end;

        end;

      end;

      assume

       A42: N is with_open_semilattices;

      let x be Point of S;

      reconsider y = x as Point of N by A1;

      consider J be Basis of y such that

       A43: for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting by A42;

      reconsider J9 = { ( uparrow A) where A be Subset of N : A in J } as Basis of x by Th16;

      take J9;

      let W be Subset of S;

      assume W in J9;

      then

      consider V be Subset of N such that

       A44: W = ( uparrow V) and

       A45: V in J;

      ( subrelstr V) is meet-inheriting by A43, A45;

      then

       A46: V is filtered by YELLOW12: 26;

      x in V by A45, YELLOW_8: 12;

      hence thesis by A46, A1, A44, WAYBEL_0: 4, WAYBEL_0: 25;

    end;

    theorem :: WAYBEL30:33

    

     Th33: for N be Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for x be Element of N holds { ( inf A) where A be Subset of S : x in A & A in ( sigma S) } c= { ( inf J) where J be Subset of N : x in J & J in ( lambda N) }

    proof

      let N be Lawson complete TopLattice, S be Scott TopAugmentation of N, x be Element of N;

      set s = { ( inf A) where A be Subset of S : x in A & A in ( sigma S) };

      let k be object;

      assume k in s;

      then

      consider J be Subset of S such that

       A1: k = ( inf J) and

       A2: x in J and

       A3: J in ( sigma S);

      

       A4: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider A = J as Subset of N;

      ( sigma N) c= ( lambda N) by Th10;

      then

       A5: ( sigma S) c= ( lambda N) by A4, YELLOW_9: 52;

      ( inf A) = ( inf J) by A4, YELLOW_0: 17, YELLOW_0: 27;

      hence thesis by A5, A1, A2, A3;

    end;

    theorem :: WAYBEL30:34

    

     Th34: for N be meet-continuous Lawson complete TopLattice holds for S be Scott TopAugmentation of N holds for x be Element of N holds { ( inf A) where A be Subset of S : x in A & A in ( sigma S) } = { ( inf J) where J be Subset of N : x in J & J in ( lambda N) }

    proof

      let N be meet-continuous Lawson complete TopLattice, S be Scott TopAugmentation of N, x be Element of N;

      set l = { ( inf A) where A be Subset of N : x in A & A in ( lambda N) }, s = { ( inf J) where J be Subset of S : x in J & J in ( sigma S) };

      thus s c= l by Th33;

      let k be object;

      assume k in l;

      then

      consider A be Subset of N such that

       A1: k = ( inf A) and

       A2: x in A and

       A3: A in ( lambda N);

      

       A4: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider J = A as Subset of S;

      A is open by A3, Th12;

      then ( uparrow J) is open by Th15;

      then

       A5: ( uparrow J) in ( sigma S) by WAYBEL14: 24;

      

       A6: J c= ( uparrow J) by WAYBEL_0: 16;

      ( inf A) = ( inf J) by A4, YELLOW_0: 17, YELLOW_0: 27

      .= ( inf ( uparrow J)) by WAYBEL_0: 38, YELLOW_0: 17;

      hence thesis by A5, A1, A2, A6;

    end;

    theorem :: WAYBEL30:35

    

     Th35: for N be meet-continuous Lawson complete TopLattice holds N is continuous iff N is with_open_semilattices & ( InclPoset ( sigma N)) is continuous

    proof

      let N be meet-continuous Lawson complete TopLattice;

      set S = the Scott TopAugmentation of N;

      

       A1: the RelStr of N = the RelStr of S by YELLOW_9:def 4;

      hereby

        assume

         A2: N is continuous;

        for x be Point of S holds ex J be Basis of x st for W be Subset of S st W in J holds W is Filter of S

        proof

          let x be Point of S;

          consider J be Basis of x such that

           A3: for W be Subset of S st W in J holds W is open filtered by A2, WAYBEL14: 35;

          take J;

          let W be Subset of S;

          assume

           A4: W in J;

          then W is open by A3;

          hence thesis by A3, A4, WAYBEL11:def 4, YELLOW_8: 12;

        end;

        hence N is with_open_semilattices by Th32;

        ( InclPoset ( sigma S)) is continuous by A2, WAYBEL14: 36;

        hence ( InclPoset ( sigma N)) is continuous by A1, YELLOW_9: 52;

      end;

      assume that

       A5: N is with_open_semilattices and

       A6: ( InclPoset ( sigma N)) is continuous;

      

       A7: for x be Element of S holds ex J be Basis of x st for Y be Subset of S st Y in J holds Y is open filtered

      proof

        let x be Element of S;

        reconsider y = x as Element of N by A1;

        consider J be Basis of y such that

         A8: for A be Subset of N st A in J holds ( subrelstr A) is meet-inheriting by A5;

        reconsider J9 = { ( uparrow A) where A be Subset of N : A in J } as Basis of x by Th16;

        take J9;

        let Y be Subset of S;

        assume

         A9: Y in J9;

        then

        consider A be Subset of N such that

         A10: Y = ( uparrow A) and

         A11: A in J;

        ( subrelstr A) is meet-inheriting by A8, A11;

        then A is filtered by YELLOW12: 26;

        hence thesis by A1, A9, A10, WAYBEL_0: 4, YELLOW_8: 12;

      end;

      ( sigma S) = ( sigma N) by A1, YELLOW_9: 52;

      then for x be Element of S holds x = ( "\/" ({ ( inf X) where X be Subset of S : x in X & X in ( sigma S) },S)) by A7, A6, WAYBEL14: 37;

      then S is continuous by WAYBEL14: 38;

      hence thesis by A1, YELLOW12: 15;

    end;

    registration

      cluster continuous -> with_open_semilattices for Lawson complete TopLattice;

      coherence by Th35;

    end

    registration

      let N be continuous Lawson complete TopLattice;

      cluster ( InclPoset ( sigma N)) -> continuous;

      coherence by Th35;

    end

    theorem :: WAYBEL30:36

    for N be continuous Lawson complete TopLattice holds N is compact Hausdorff topological_semilattice with_open_semilattices

    proof

      let N be continuous Lawson complete TopLattice;

      thus N is compact Hausdorff;

      ( InclPoset ( sigma N)) is continuous;

      hence N is topological_semilattice by Th22;

      thus thesis;

    end;

    theorem :: WAYBEL30:37

    for N be Hausdorff topological_semilattice with_open_semilattices Lawson complete TopLattice holds N is with_compact_semilattices

    proof

      let N be Hausdorff topological_semilattice with_open_semilattices Lawson complete TopLattice;

      let x be Point of N;

      consider BO be Basis of x such that

       A1: for A be Subset of N st A in BO holds ( subrelstr A) is meet-inheriting by Def4;

      set BC = { ( Cl A) where A be Subset of N : A in BO };

      BC c= ( bool the carrier of N)

      proof

        let k be object;

        assume k in BC;

        then ex A be Subset of N st k = ( Cl A) & A in BO;

        hence thesis;

      end;

      then

      reconsider BC as Subset-Family of N;

      BC is basis of x

      proof

        let S be a_neighborhood of x;

        

         A2: ( Int S) c= S by TOPS_1: 16;

        x in ( Int S) by CONNSP_2:def 1;

        then

        consider W be Subset of N such that

         A3: W in BO and

         A4: W c= ( Int S) by YELLOW_8: 13;

        

         A5: W is open by A3, YELLOW_8: 12;

        x in W by A3, YELLOW_8: 12;

        then x in ( Int W) by A5, TOPS_1: 23;

        then

        reconsider T = W as a_neighborhood of x by CONNSP_2:def 1;

        per cases ;

          suppose

           A6: W <> ( [#] N);

          x in W by A3, YELLOW_8: 12;

          then {x} c= W by ZFMISC_1: 31;

          then

          consider G be Subset of N such that

           A7: G is open and

           A8: {x} c= G and

           A9: ( Cl G) c= W by A5, A6, CONNSP_2: 20;

          x in G by A8, ZFMISC_1: 31;

          then

          consider K be Subset of N such that

           A10: K in BO and

           A11: K c= G by A7, YELLOW_8: 13;

          

           A12: K is open by A10, YELLOW_8: 12;

          

           A13: ( Int K) c= ( Int ( Cl K)) by PRE_TOPC: 18, TOPS_1: 19;

          x in K by A10, YELLOW_8: 12;

          then x in ( Int K) by A12, TOPS_1: 23;

          then

          reconsider KK = ( Cl K) as a_neighborhood of x by A13, CONNSP_2:def 1;

          take KK;

          thus KK in BC by A10;

          ( Cl K) c= ( Cl G) by A11, PRE_TOPC: 19;

          then ( Cl K) c= W by A9;

          then KK c= ( Int S) by A4;

          hence thesis by A2;

        end;

          suppose

           A14: W = ( [#] N);

          take T;

          ( Cl ( [#] N)) = ( [#] N) by TOPS_1: 2;

          hence T in BC by A3, A14;

          thus thesis by A4, A2;

        end;

      end;

      then

      reconsider BC as basis of x;

      take BC;

      let A be Subset of N;

      assume A in BC;

      then

      consider C be Subset of N such that

       A15: A = ( Cl C) and

       A16: C in BO;

      ( subrelstr C) is meet-inheriting by A1, A16;

      hence ( subrelstr A) is meet-inheriting by A15, Th31;

      thus thesis by A15, COMPTS_1: 8;

    end;

    theorem :: WAYBEL30:38

    for N be meet-continuous Hausdorff Lawson complete TopLattice, x be Element of N holds x = ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N))

    proof

      let N be meet-continuous Hausdorff Lawson complete TopLattice, x be Element of N;

      set S = the Scott complete TopAugmentation of N;

      

       A1: ( InclPoset ( sigma S)) is continuous by WAYBEL14: 36;

      

       A2: the RelStr of S = the RelStr of N by YELLOW_9:def 4;

      then

      reconsider y = x as Element of S;

      for y be Element of S holds ex J be Basis of y st for X be Subset of S st X in J holds X is open filtered by WAYBEL14: 35;

      

      hence x = ( "\/" ({ ( inf X) where X be Subset of S : y in X & X in ( sigma S) },S)) by A1, WAYBEL14: 37

      .= ( "\/" ({ ( inf X) where X be Subset of S : x in X & X in ( sigma S) },N)) by A2, YELLOW_0: 17, YELLOW_0: 26

      .= ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N)) by Th34;

    end;

    theorem :: WAYBEL30:39

    for N be meet-continuous Lawson complete TopLattice holds N is continuous iff for x be Element of N holds x = ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N))

    proof

      let N be meet-continuous Lawson complete TopLattice;

      set S = the complete Scott TopAugmentation of N;

      

       A1: the RelStr of S = the RelStr of N by YELLOW_9:def 4;

      hereby

        assume

         A2: N is continuous;

        then

         A3: for x be Element of S holds ex J be Basis of x st for Y be Subset of S st Y in J holds Y is open filtered by WAYBEL14: 35;

        let x be Element of N;

        ( InclPoset ( sigma S)) is continuous by A2, WAYBEL14: 36;

        

        hence x = ( "\/" ({ ( inf X) where X be Subset of S : x in X & X in ( sigma S) },S)) by A3, A1, WAYBEL14: 37

        .= ( "\/" ({ ( inf X) where X be Subset of S : x in X & X in ( sigma S) },N)) by A1, YELLOW_0: 17, YELLOW_0: 26

        .= ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N)) by Th34;

      end;

      assume

       A4: for x be Element of N holds x = ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N));

      now

        let x be Element of S;

        

        thus x = ( "\/" ({ ( inf V) where V be Subset of N : x in V & V in ( lambda N) },N)) by A1, A4

        .= ( "\/" ({ ( inf V) where V be Subset of S : x in V & V in ( sigma S) },N)) by A1, Th34

        .= ( "\/" ({ ( inf V) where V be Subset of S : x in V & V in ( sigma S) },S)) by A1, YELLOW_0: 17, YELLOW_0: 26;

      end;

      then S is continuous by WAYBEL14: 38;

      hence thesis by A1, YELLOW12: 15;

    end;

    theorem :: WAYBEL30:40

    

     Th40: for N be meet-continuous Lawson complete TopLattice holds N is algebraic iff N is with_open_semilattices & ( InclPoset ( sigma N)) is algebraic

    proof

      let N be meet-continuous Lawson complete TopLattice;

      set S = the Scott TopAugmentation of N;

      

       A1: the RelStr of S = the RelStr of N by YELLOW_9:def 4;

      hereby

        assume

         A2: N is algebraic;

        then

        reconsider M = N as algebraic LATTICE;

        M is continuous;

        hence N is with_open_semilattices;

        S is algebraic by A1, A2, WAYBEL_8: 17;

        then ex K be Basis of S st K = { ( uparrow x) where x be Element of S : x in the carrier of ( CompactSublatt S) } by WAYBEL14: 42;

        then ( InclPoset ( sigma S)) is algebraic by WAYBEL14: 43;

        hence ( InclPoset ( sigma N)) is algebraic by A1, YELLOW_9: 52;

      end;

      assume that

       A3: N is with_open_semilattices and

       A4: ( InclPoset ( sigma N)) is algebraic;

      reconsider T = ( InclPoset ( sigma N)) as algebraic LATTICE by A4;

      T is continuous;

      then N is continuous by A3, Th35;

      then for x be Element of S holds ex K be Basis of x st for Y be Subset of S st Y in K holds Y is open filtered by WAYBEL14: 35;

      then

       A5: for V be Element of ( InclPoset ( sigma S)) holds ex VV be Subset of ( InclPoset ( sigma S)) st V = ( sup VV) & for W be Element of ( InclPoset ( sigma S)) st W in VV holds W is co-prime by WAYBEL14: 39;

      ( InclPoset ( sigma S)) is algebraic by A1, A4, YELLOW_9: 52;

      then ex K be Basis of S st K = { ( uparrow x) where x be Element of S : x in the carrier of ( CompactSublatt S) } by A5, WAYBEL14: 44;

      then S is algebraic by WAYBEL14: 45;

      hence thesis by A1, WAYBEL_8: 17;

    end;

    registration

      let N be meet-continuous algebraic Lawson complete TopLattice;

      cluster ( InclPoset ( sigma N)) -> algebraic;

      coherence by Th40;

    end