waybel12.miz



    begin

    

     Lm1: for L be non empty RelStr, f be sequence of the carrier of L holds for n be Element of NAT holds { (f . k) where k be Element of NAT : k <= n } is non empty finite Subset of L

    proof

      let L be non empty RelStr, f be sequence of the carrier of L, n be Element of NAT ;

      set A = { (f . m) where m be Element of NAT : m <= n };

      

       A1: A c= { (f . m) where m be Element of NAT : m in ( { 0 } \/ ( Seg n)) }

      proof

        let q be object;

        assume q in A;

        then

        consider m be Element of NAT such that

         A2: q = (f . m) and

         A3: m <= n;

        

         A4: m = 0 or m in ( Seg m) by FINSEQ_1: 3;

        ( Seg m) c= ( Seg n) by A3, FINSEQ_1: 5;

        then m in { 0 } or m in ( Seg n) by A4, TARSKI:def 1;

        then m in ( { 0 } \/ ( Seg n)) by XBOOLE_0:def 3;

        hence thesis by A2;

      end;

      deffunc F( set) = (f . $1);

      

       A5: A c= the carrier of L

      proof

        let q be object;

        assume q in A;

        then ex m be Element of NAT st q = (f . m) & m <= n;

        hence thesis;

      end;

      ( card { F(m) where m be Element of NAT : m in ( { 0 } \/ ( Seg n)) }) c= ( card ( { 0 } \/ ( Seg n))) from TREES_2:sch 2;

      then

       A6: { (f . m) where m be Element of NAT : m in ( { 0 } \/ ( Seg n)) } is finite;

       0 <= n by NAT_1: 2;

      then (f . 0 ) in A;

      hence thesis by A1, A6, A5;

    end;

    definition

      let T be TopStruct, P be Subset of T;

      :: original: closed

      redefine

      :: WAYBEL12:def1

      attr P is closed means (P ` ) is open;

      compatibility ;

    end

    definition

      let T be TopStruct, F be Subset-Family of T;

      :: WAYBEL12:def2

      attr F is dense means for X be Subset of T st X in F holds X is dense;

    end

    theorem :: WAYBEL12:1

    

     Th1: for X,Y be set st ( card X) c= ( card Y) & Y is countable holds X is countable

    proof

      let X,Y be set such that

       A1: ( card X) c= ( card Y);

      assume ( card Y) c= omega ;

      hence ( card X) c= omega by A1;

    end;

    theorem :: WAYBEL12:2

    for A be denumerable set holds ( NAT ,A) are_equipotent

    proof

      let A be denumerable set;

       not ( card A) in omega ;

      then

       A1: omega c= ( card A) by CARD_1: 4;

      ( card A) c= omega by CARD_3:def 14;

      then ( card NAT ) = ( card A) by A1;

      hence thesis by CARD_1: 5;

    end;

    theorem :: WAYBEL12:3

    for L be non empty transitive RelStr, A,B be Subset of L st A is_finer_than B holds ( downarrow A) c= ( downarrow B)

    proof

      let L be non empty transitive RelStr, A,B be Subset of L such that

       A1: for a be Element of L st a in A holds ex b be Element of L st b in B & b >= a;

      let q be object;

      assume

       A2: q in ( downarrow A);

      then

      reconsider q1 = q as Element of L;

      consider a be Element of L such that

       A3: a >= q1 and

       A4: a in A by A2, WAYBEL_0:def 15;

      consider b be Element of L such that

       A5: b in B and

       A6: b >= a by A1, A4;

      b >= q1 by A3, A6, ORDERS_2: 3;

      hence thesis by A5, WAYBEL_0:def 15;

    end;

    theorem :: WAYBEL12:4

    

     Th4: for L be non empty transitive RelStr, A,B be Subset of L st A is_coarser_than B holds ( uparrow A) c= ( uparrow B)

    proof

      let L be non empty transitive RelStr, A,B be Subset of L such that

       A1: for a be Element of L st a in A holds ex b be Element of L st b in B & b <= a;

      let q be object;

      assume

       A2: q in ( uparrow A);

      then

      reconsider q1 = q as Element of L;

      consider a be Element of L such that

       A3: a <= q1 and

       A4: a in A by A2, WAYBEL_0:def 16;

      consider b be Element of L such that

       A5: b in B and

       A6: b <= a by A1, A4;

      b <= q1 by A3, A6, ORDERS_2: 3;

      hence thesis by A5, WAYBEL_0:def 16;

    end;

    theorem :: WAYBEL12:5

    for L be non empty Poset, D be non empty finite filtered Subset of L st ex_inf_of (D,L) holds ( inf D) in D

    proof

      let L be non empty Poset, D be non empty finite filtered Subset of L such that

       A1: ex_inf_of (D,L);

      D c= D;

      then

      consider d be Element of L such that

       A2: d in D and

       A3: d is_<=_than D by WAYBEL_0: 2;

      

       A4: ( inf D) >= d by A1, A3, YELLOW_0: 31;

      ( inf D) is_<=_than D by A1, YELLOW_0: 31;

      then ( inf D) <= d by A2;

      hence thesis by A2, A4, ORDERS_2: 2;

    end;

    theorem :: WAYBEL12:6

    for L be lower-bounded antisymmetric non empty RelStr holds for X be non empty lower Subset of L holds ( Bottom L) in X

    proof

      let L be lower-bounded antisymmetric non empty RelStr, X be non empty lower Subset of L;

      consider y be object such that

       A1: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A1;

      ( Bottom L) <= y by YELLOW_0: 44;

      hence thesis by WAYBEL_0:def 19;

    end;

    theorem :: WAYBEL12:7

    for L be lower-bounded antisymmetric non empty RelStr holds for X be non empty Subset of L holds ( Bottom L) in ( downarrow X)

    proof

      let L be lower-bounded antisymmetric non empty RelStr, X be non empty Subset of L;

      consider y be object such that

       A1: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A1;

      ( downarrow X) = { x where x be Element of L : ex y be Element of L st x <= y & y in X } & ( Bottom L) <= y by WAYBEL_0: 14, YELLOW_0: 44;

      hence thesis;

    end;

    theorem :: WAYBEL12:8

    

     Th8: for L be upper-bounded antisymmetric non empty RelStr holds for X be non empty upper Subset of L holds ( Top L) in X

    proof

      let L be upper-bounded antisymmetric non empty RelStr, X be non empty upper Subset of L;

      consider y be object such that

       A1: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A1;

      ( Top L) >= y by YELLOW_0: 45;

      hence thesis by WAYBEL_0:def 20;

    end;

    theorem :: WAYBEL12:9

    

     Th9: for L be upper-bounded antisymmetric non empty RelStr holds for X be non empty Subset of L holds ( Top L) in ( uparrow X)

    proof

      let L be upper-bounded antisymmetric non empty RelStr, X be non empty Subset of L;

      consider y be object such that

       A1: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A1;

      ( uparrow X) = { x where x be Element of L : ex y be Element of L st x >= y & y in X } & ( Top L) >= y by WAYBEL_0: 15, YELLOW_0: 45;

      hence thesis;

    end;

    theorem :: WAYBEL12:10

    

     Th10: for L be lower-bounded with_infima antisymmetric RelStr holds for X be Subset of L holds (X "/\" {( Bottom L)}) c= {( Bottom L)}

    proof

      let L be lower-bounded with_infima antisymmetric RelStr, X be Subset of L;

      

       A1: ( {( Bottom L)} "/\" X) = { (( Bottom L) "/\" y) where y be Element of L : y in X } by YELLOW_4: 42;

      let q be object;

      assume q in (X "/\" {( Bottom L)});

      then

      consider y be Element of L such that

       A2: q = (( Bottom L) "/\" y) and y in X by A1;

      (y "/\" ( Bottom L)) = ( Bottom L) by WAYBEL_1: 3;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: WAYBEL12:11

    for L be lower-bounded with_infima antisymmetric RelStr holds for X be non empty Subset of L holds (X "/\" {( Bottom L)}) = {( Bottom L)}

    proof

      let L be lower-bounded with_infima antisymmetric RelStr, X be non empty Subset of L;

      thus (X "/\" {( Bottom L)}) c= {( Bottom L)} by Th10;

      let q be object;

      assume q in {( Bottom L)};

      then

       A1: (X "/\" {( Bottom L)}) = { (( Bottom L) "/\" y) where y be Element of L : y in X } & q = ( Bottom L) by TARSKI:def 1, YELLOW_4: 42;

      consider y be object such that

       A2: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A2;

      (( Bottom L) "/\" y) = ( Bottom L) by WAYBEL_1: 3;

      hence thesis by A1;

    end;

    theorem :: WAYBEL12:12

    

     Th12: for L be upper-bounded with_suprema antisymmetric RelStr holds for X be Subset of L holds (X "\/" {( Top L)}) c= {( Top L)}

    proof

      let L be upper-bounded with_suprema antisymmetric RelStr, X be Subset of L;

      

       A1: ( {( Top L)} "\/" X) = { (( Top L) "\/" y) where y be Element of L : y in X } by YELLOW_4: 15;

      let q be object;

      assume q in (X "\/" {( Top L)});

      then

      consider y be Element of L such that

       A2: q = (( Top L) "\/" y) and y in X by A1;

      (y "\/" ( Top L)) = ( Top L) by WAYBEL_1: 4;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: WAYBEL12:13

    for L be upper-bounded with_suprema antisymmetric RelStr holds for X be non empty Subset of L holds (X "\/" {( Top L)}) = {( Top L)}

    proof

      let L be upper-bounded with_suprema antisymmetric RelStr, X be non empty Subset of L;

      thus (X "\/" {( Top L)}) c= {( Top L)} by Th12;

      let q be object;

      assume q in {( Top L)};

      then

       A1: (X "\/" {( Top L)}) = { (( Top L) "\/" y) where y be Element of L : y in X } & q = ( Top L) by TARSKI:def 1, YELLOW_4: 15;

      consider y be object such that

       A2: y in X by XBOOLE_0:def 1;

      reconsider y as Element of X by A2;

      (( Top L) "\/" y) = ( Top L) by WAYBEL_1: 4;

      hence thesis by A1;

    end;

    theorem :: WAYBEL12:14

    

     Th14: for L be upper-bounded Semilattice, X be Subset of L holds ( {( Top L)} "/\" X) = X

    proof

      let L be upper-bounded Semilattice, X be Subset of L;

      

       A1: ( {( Top L)} "/\" X) = { (( Top L) "/\" y) where y be Element of L : y in X } by YELLOW_4: 42;

      thus ( {( Top L)} "/\" X) c= X

      proof

        let q be object;

        assume q in ( {( Top L)} "/\" X);

        then ex y be Element of L st q = (( Top L) "/\" y) & y in X by A1;

        hence thesis by WAYBEL_1: 4;

      end;

      let q be object;

      assume

       A2: q in X;

      then

      reconsider X1 = X as non empty Subset of L;

      reconsider y = q as Element of X1 by A2;

      q = (( Top L) "/\" y) by WAYBEL_1: 4;

      hence thesis by A1;

    end;

    theorem :: WAYBEL12:15

    for L be lower-bounded with_suprema Poset, X be Subset of L holds ( {( Bottom L)} "\/" X) = X

    proof

      let L be lower-bounded with_suprema Poset, X be Subset of L;

      

       A1: ( {( Bottom L)} "\/" X) = { (( Bottom L) "\/" y) where y be Element of L : y in X } by YELLOW_4: 15;

      thus ( {( Bottom L)} "\/" X) c= X

      proof

        let q be object;

        assume q in ( {( Bottom L)} "\/" X);

        then ex y be Element of L st q = (( Bottom L) "\/" y) & y in X by A1;

        hence thesis by WAYBEL_1: 3;

      end;

      let q be object;

      assume

       A2: q in X;

      then

      reconsider X1 = X as non empty Subset of L;

      reconsider y = q as Element of X1 by A2;

      q = (( Bottom L) "\/" y) by WAYBEL_1: 3;

      hence thesis by A1;

    end;

    theorem :: WAYBEL12:16

    

     Th16: for L be non empty reflexive RelStr, A,B be Subset of L st A c= B holds A is_finer_than B & A is_coarser_than B

    proof

      let L be non empty reflexive RelStr, A,B be Subset of L such that

       A1: A c= B;

      thus A is_finer_than B

      proof

        let a be Element of L such that

         A2: a in A;

        take b = a;

        thus b in B & a <= b by A1, A2;

      end;

      let a be Element of L such that

       A3: a in A;

      take b = a;

      thus b in B & b <= a by A1, A3;

    end;

    theorem :: WAYBEL12:17

    

     Th17: for L be antisymmetric transitive with_infima RelStr holds for V be Subset of L, x,y be Element of L st x <= y holds ( {y} "/\" V) is_coarser_than ( {x} "/\" V)

    proof

      let L be antisymmetric transitive with_infima RelStr, V be Subset of L, x,y be Element of L such that

       A1: x <= y;

      

       A2: ( {y} "/\" V) = { (y "/\" s) where s be Element of L : s in V } by YELLOW_4: 42;

      let b be Element of L;

      assume b in ( {y} "/\" V);

      then

      consider s be Element of L such that

       A3: b = (y "/\" s) and

       A4: s in V by A2;

      take a = (x "/\" s);

      ( {x} "/\" V) = { (x "/\" t) where t be Element of L : t in V } by YELLOW_4: 42;

      hence a in ( {x} "/\" V) by A4;

      thus thesis by A1, A3, WAYBEL_1: 1;

    end;

    theorem :: WAYBEL12:18

    for L be antisymmetric transitive with_suprema RelStr holds for V be Subset of L, x,y be Element of L st x <= y holds ( {x} "\/" V) is_finer_than ( {y} "\/" V)

    proof

      let L be antisymmetric transitive with_suprema RelStr, V be Subset of L, x,y be Element of L such that

       A1: x <= y;

      

       A2: ( {x} "\/" V) = { (x "\/" s) where s be Element of L : s in V } by YELLOW_4: 15;

      let b be Element of L;

      assume b in ( {x} "\/" V);

      then

      consider s be Element of L such that

       A3: b = (x "\/" s) and

       A4: s in V by A2;

      take a = (y "\/" s);

      ( {y} "\/" V) = { (y "\/" t) where t be Element of L : t in V } by YELLOW_4: 15;

      hence a in ( {y} "\/" V) by A4;

      thus thesis by A1, A3, WAYBEL_1: 2;

    end;

    theorem :: WAYBEL12:19

    

     Th19: for L be non empty RelStr, V,S,T be Subset of L st S is_coarser_than T & V is upper & T c= V holds S c= V

    proof

      let L be non empty RelStr, V,S,T be Subset of L such that

       A1: S is_coarser_than T and

       A2: V is upper & T c= V;

      let q be object;

      assume

       A3: q in S;

      then

      reconsider S1 = S as non empty Subset of L;

      reconsider b = q as Element of S1 by A3;

      ex a be Element of L st a in T & a <= b by A1;

      hence thesis by A2;

    end;

    theorem :: WAYBEL12:20

    for L be non empty RelStr, V,S,T be Subset of L st S is_finer_than T & V is lower & T c= V holds S c= V

    proof

      let L be non empty RelStr, V,S,T be Subset of L such that

       A1: S is_finer_than T and

       A2: V is lower & T c= V;

      let q be object;

      assume

       A3: q in S;

      then

      reconsider S1 = S as non empty Subset of L;

      reconsider a = q as Element of S1 by A3;

      ex b be Element of L st b in T & a <= b by A1;

      hence thesis by A2;

    end;

    theorem :: WAYBEL12:21

    

     Th21: for L be Semilattice, F be upper filtered Subset of L holds (F "/\" F) = F

    proof

      let L be Semilattice, F be upper filtered Subset of L;

      thus (F "/\" F) c= F

      proof

        let x be object;

        assume x in (F "/\" F);

        then

        consider y,z be Element of L such that

         A1: x = (y "/\" z) and

         A2: y in F & z in F;

        consider t be Element of L such that

         A3: t in F and

         A4: t <= y & t <= z by A2, WAYBEL_0:def 2;

        (y "/\" z) >= t by A4, YELLOW_0: 23;

        hence thesis by A1, A3, WAYBEL_0:def 20;

      end;

      thus thesis by YELLOW_4: 40;

    end;

    theorem :: WAYBEL12:22

    for L be sup-Semilattice, I be lower directed Subset of L holds (I "\/" I) = I

    proof

      let L be sup-Semilattice, I be lower directed Subset of L;

      thus (I "\/" I) c= I

      proof

        let x be object;

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

        then

        consider y,z be Element of L such that

         A1: x = (y "\/" z) and

         A2: y in I & z in I;

        consider t be Element of L such that

         A3: t in I and

         A4: t >= y & t >= z by A2, WAYBEL_0:def 1;

        (y "\/" z) <= t by A4, YELLOW_0: 22;

        hence thesis by A1, A3, WAYBEL_0:def 19;

      end;

      thus thesis by YELLOW_4: 13;

    end;

    

     Lm2: for L be non empty RelStr, V be Subset of L holds { x where x be Element of L : (V "/\" {x}) c= V } is Subset of L

    proof

      let L be non empty RelStr, V be Subset of L;

      set G = { x where x be Element of L : (V "/\" {x}) c= V };

      G c= the carrier of L

      proof

        let q be object;

        assume q in G;

        then ex x be Element of L st q = x & (V "/\" {x}) c= V;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL12:23

    

     Th23: for L be upper-bounded Semilattice, V be Subset of L holds { x where x be Element of L : (V "/\" {x}) c= V } is non empty

    proof

      let L be upper-bounded Semilattice, V be Subset of L;

      set G = { x where x be Element of L : (V "/\" {x}) c= V };

      (V "/\" {( Top L)}) = V by Th14;

      then ( Top L) in G;

      hence thesis;

    end;

    theorem :: WAYBEL12:24

    

     Th24: for L be antisymmetric transitive with_infima RelStr, V be Subset of L holds { x where x be Element of L : (V "/\" {x}) c= V } is filtered Subset of L

    proof

      let L be antisymmetric transitive with_infima RelStr, V be Subset of L;

      reconsider G1 = { x where x be Element of L : (V "/\" {x}) c= V } as Subset of L by Lm2;

      G1 is filtered

      proof

        let x,y be Element of L;

        assume x in G1;

        then

        consider x1 be Element of L such that

         A1: x = x1 and

         A2: (V "/\" {x1}) c= V;

        assume y in G1;

        then

        consider y1 be Element of L such that

         A3: y = y1 and

         A4: (V "/\" {y1}) c= V;

        take z = (x1 "/\" y1);

        (V "/\" {z}) c= V

        proof

          

           A5: ( {z} "/\" V) = { (z "/\" v) where v be Element of L : v in V } by YELLOW_4: 42;

          let q be object;

          assume q in (V "/\" {z});

          then

          consider v be Element of L such that

           A6: q = (z "/\" v) and

           A7: v in V by A5;

          

           A8: ( {x1} "/\" V) = { (x1 "/\" s) where s be Element of L : s in V } & q = (x1 "/\" (y1 "/\" v)) by A6, LATTICE3: 16, YELLOW_4: 42;

          ( {y1} "/\" V) = { (y1 "/\" t) where t be Element of L : t in V } by YELLOW_4: 42;

          then (y1 "/\" v) in (V "/\" {y1}) by A7;

          then q in (V "/\" {x1}) by A4, A8;

          hence thesis by A2;

        end;

        hence z in G1;

        thus thesis by A1, A3, YELLOW_0: 23;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL12:25

    

     Th25: for L be antisymmetric transitive with_infima RelStr holds for V be upper Subset of L holds { x where x be Element of L : (V "/\" {x}) c= V } is upper Subset of L

    proof

      let L be antisymmetric transitive with_infima RelStr, V be upper Subset of L;

      reconsider G1 = { x where x be Element of L : (V "/\" {x}) c= V } as Subset of L by Lm2;

      G1 is upper

      proof

        let x,y be Element of L;

        assume x in G1;

        then

         A1: ex x1 be Element of L st x1 = x & (V "/\" {x1}) c= V;

        assume x <= y;

        then (V "/\" {y}) c= V by A1, Th17, Th19;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL12:26

    

     Th26: for L be with_infima Poset, X be Subset of L st X is Open lower holds X is filtered

    proof

      let L be with_infima Poset, X be Subset of L such that

       A1: X is Open lower;

      let x,y be Element of L such that

       A2: x in X and y in X;

      

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

      then (x "/\" y) in X by A1, A2;

      then

      consider z be Element of L such that

       A4: z in X and

       A5: z << (x "/\" y) by A1;

      take z;

      (x "/\" y) <= y & z <= (x "/\" y) by A5, WAYBEL_3: 1, YELLOW_0: 23;

      hence z in X & z <= x & z <= y by A3, A4, ORDERS_2: 3;

    end;

    registration

      let L be with_infima Poset;

      cluster Open lower -> filtered for Subset of L;

      coherence by Th26;

    end

    registration

      let L be continuous antisymmetric non empty reflexive RelStr;

      cluster lower -> Open for Subset of L;

      coherence

      proof

        let A be Subset of L such that

         A1: A is lower;

        let x be Element of L such that

         A2: x in A;

        consider y be object such that

         A3: y in ( waybelow x) by XBOOLE_0:def 1;

        reconsider y as Element of L by A3;

        take y;

        y << x by A3, WAYBEL_3: 7;

        then y <= x by WAYBEL_3: 1;

        hence thesis by A1, A2, A3, WAYBEL_3: 7;

      end;

    end

    registration

      let L be continuous Semilattice, x be Element of L;

      cluster (( downarrow x) ` ) -> Open;

      coherence

      proof

        let a be Element of L;

        set A = (( downarrow x) ` );

        assume a in A;

        then not a in ( downarrow x) by XBOOLE_0:def 5;

        then

         A1: not a <= x by WAYBEL_0: 17;

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

        then

        consider y be Element of L such that

         A2: y << a and

         A3: not y <= x by A1, WAYBEL_3: 24;

        take y;

         not y in ( downarrow x) by A3, WAYBEL_0: 17;

        hence y in A by XBOOLE_0:def 5;

        thus thesis by A2;

      end;

    end

    theorem :: WAYBEL12:27

    

     Th27: for L be Semilattice, C be non empty Subset of L st for x,y be Element of L st x in C & y in C holds x <= y or y <= x holds for Y be non empty finite Subset of C holds ( "/\" (Y,L)) in Y

    proof

      let L be Semilattice, C be non empty Subset of L such that

       A1: for x,y be Element of L st x in C & y in C holds x <= y or y <= x;

      defpred P[ set] means ( "/\" ($1,L)) in $1 & ex_inf_of ($1,L);

      

       A2: for B1,B2 be non empty Element of ( Fin C) holds P[B1] & P[B2] implies P[(B1 \/ B2)]

      proof

        let B1,B2 be non empty Element of ( Fin C) such that

         A3: P[B1] & P[B2];

        B1 c= C & B2 c= C by FINSUB_1:def 5;

        then ( "/\" (B1,L)) <= ( "/\" (B2,L)) or ( "/\" (B2,L)) <= ( "/\" (B1,L)) by A1, A3;

        then

         A4: (( "/\" (B1,L)) "/\" ( "/\" (B2,L))) = ( "/\" (B1,L)) or (( "/\" (B1,L)) "/\" ( "/\" (B2,L))) = ( "/\" (B2,L)) by YELLOW_0: 25;

        ( "/\" ((B1 \/ B2),L)) = (( "/\" (B1,L)) "/\" ( "/\" (B2,L))) by A3, YELLOW_2: 4;

        hence thesis by A3, A4, XBOOLE_0:def 3, YELLOW_2: 4;

      end;

      let Y be non empty finite Subset of C;

      

       A5: Y in ( Fin C) by FINSUB_1:def 5;

      

       A6: for x be Element of C holds P[ {x}]

      proof

        let x be Element of C;

        ( "/\" ( {x},L)) = x by YELLOW_0: 39;

        hence thesis by TARSKI:def 1, YELLOW_0: 38;

      end;

      for B be non empty Element of ( Fin C) holds P[B] from SETWISEO:sch 3( A6, A2);

      hence thesis by A5;

    end;

    theorem :: WAYBEL12:28

    for L be sup-Semilattice, C be non empty Subset of L st for x,y be Element of L st x in C & y in C holds x <= y or y <= x holds for Y be non empty finite Subset of C holds ( "\/" (Y,L)) in Y

    proof

      let L be sup-Semilattice, C be non empty Subset of L such that

       A1: for x,y be Element of L st x in C & y in C holds x <= y or y <= x;

      defpred P[ set] means ( "\/" ($1,L)) in $1 & ex_sup_of ($1,L);

      

       A2: for B1,B2 be non empty Element of ( Fin C) holds P[B1] & P[B2] implies P[(B1 \/ B2)]

      proof

        let B1,B2 be non empty Element of ( Fin C) such that

         A3: P[B1] & P[B2];

        B1 c= C & B2 c= C by FINSUB_1:def 5;

        then ( "\/" (B1,L)) <= ( "\/" (B2,L)) or ( "\/" (B2,L)) <= ( "\/" (B1,L)) by A1, A3;

        then

         A4: (( "\/" (B1,L)) "\/" ( "\/" (B2,L))) = ( "\/" (B1,L)) or (( "\/" (B1,L)) "\/" ( "\/" (B2,L))) = ( "\/" (B2,L)) by YELLOW_0: 24;

        ( "\/" ((B1 \/ B2),L)) = (( "\/" (B1,L)) "\/" ( "\/" (B2,L))) by A3, YELLOW_2: 3;

        hence thesis by A3, A4, XBOOLE_0:def 3, YELLOW_2: 3;

      end;

      let Y be non empty finite Subset of C;

      

       A5: Y in ( Fin C) by FINSUB_1:def 5;

      

       A6: for x be Element of C holds P[ {x}]

      proof

        let x be Element of C;

        ( "\/" ( {x},L)) = x by YELLOW_0: 39;

        hence thesis by TARSKI:def 1, YELLOW_0: 38;

      end;

      for B be non empty Element of ( Fin C) holds P[B] from SETWISEO:sch 3( A6, A2);

      hence thesis by A5;

    end;

    

     Lm3: for L be Semilattice, F be Filter of L holds F = ( uparrow ( fininfs F)) by WAYBEL_0: 62;

    definition

      let L be Semilattice, F be Filter of L;

      :: WAYBEL12:def3

      mode GeneratorSet of F -> Subset of L means

      : Def3: F = ( uparrow ( fininfs it ));

      existence

      proof

        take F;

        thus thesis by Lm3;

      end;

    end

    registration

      let L be Semilattice, F be Filter of L;

      cluster non empty for GeneratorSet of F;

      existence

      proof

        F = ( uparrow ( fininfs F)) by Lm3;

        then

        reconsider F1 = F as GeneratorSet of F by Def3;

        take F1;

        thus thesis;

      end;

    end

    

     Lm4: for L be Semilattice, F be Filter of L holds for G be GeneratorSet of F holds G c= F

    proof

      let L be Semilattice, F be Filter of L, G be GeneratorSet of F;

      F = ( uparrow ( fininfs G)) by Def3;

      hence thesis by WAYBEL_0: 62;

    end;

    theorem :: WAYBEL12:29

    

     Th29: for L be Semilattice, A be Subset of L holds for B be non empty Subset of L st A is_coarser_than B holds ( fininfs A) is_coarser_than ( fininfs B)

    proof

      let L be Semilattice, A be Subset of L, B be non empty Subset of L such that

       A1: for a be Element of L st a in A holds ex b be Element of L st b in B & b <= a;

      defpred P[ object, object] means ex x,y be Element of L st x = $1 & y = $2 & y <= x;

      let a be Element of L;

      assume a in ( fininfs A);

      then

      consider Y be finite Subset of A such that

       A2: a = ( "/\" (Y,L)) and

       A3: ex_inf_of (Y,L);

      

       A4: for e be object st e in Y holds ex u be object st u in B & P[e, u]

      proof

        let e be object such that

         A5: e in Y;

        Y c= the carrier of L by XBOOLE_1: 1;

        then

        reconsider e as Element of L by A5;

        ex b be Element of L st b in B & b <= e by A1, A5;

        hence thesis;

      end;

      consider f be Function of Y, B such that

       A6: for e be object st e in Y holds P[e, (f . e)] from FUNCT_2:sch 1( A4);

      

       A7: (f .: Y) c= the carrier of L

      proof

        let y be object;

        assume y in (f .: Y);

        then

        consider x be object such that

         A8: x in ( dom f) and x in Y and

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

        (f . x) in B by A8, FUNCT_2: 5;

        hence thesis by A9;

      end;

       A10:

      now

        per cases ;

          case Y = {} ;

          hence ex_inf_of ((f .: Y),L) by A3;

        end;

          case Y <> {} ;

          then

          consider e be object such that

           A11: e in Y by XBOOLE_0:def 1;

          ( dom f) = Y by FUNCT_2:def 1;

          then (f . e) in (f .: Y) by A11, FUNCT_1:def 6;

          hence ex_inf_of ((f .: Y),L) by A7, YELLOW_0: 55;

        end;

      end;

      ( "/\" ((f .: Y),L)) is_<=_than Y

      proof

        let e be Element of L;

        assume

         A12: e in Y;

        then

        consider x,y be Element of L such that

         A13: x = e and

         A14: y = (f . e) and

         A15: y <= x by A6;

        ( dom f) = Y by FUNCT_2:def 1;

        then (f . e) in (f .: Y) by A12, FUNCT_1:def 6;

        then ( "/\" ((f .: Y),L)) <= y by A10, A14, YELLOW_4: 2;

        hence ( "/\" ((f .: Y),L)) <= e by A13, A15, ORDERS_2: 3;

      end;

      then

       A16: ( "/\" ((f .: Y),L)) <= ( "/\" (Y,L)) by A3, YELLOW_0: 31;

      ( "/\" ((f .: Y),L)) in ( fininfs B) by A10;

      hence ex b be Element of L st b in ( fininfs B) & b <= a by A2, A16;

    end;

    theorem :: WAYBEL12:30

    

     Th30: for L be Semilattice, F be Filter of L, G be GeneratorSet of F holds for A be non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds A is GeneratorSet of F

    proof

      let L be Semilattice, F be Filter of L, G be GeneratorSet of F, A be non empty Subset of L such that

       A1: G is_coarser_than A;

      assume

       A2: A is_coarser_than F;

      F = ( uparrow ( fininfs G)) by Def3;

      hence F c= ( uparrow ( fininfs A)) by A1, Th4, Th29;

      A c= F by A2, YELLOW_4: 8;

      hence thesis by WAYBEL_0: 62;

    end;

    theorem :: WAYBEL12:31

    

     Th31: for L be Semilattice, A be Subset of L holds for f,g be sequence of the carrier of L st ( rng f) = A & for n be Element of NAT holds (g . n) = ( "/\" ({ (f . m) where m be Element of NAT : m <= n },L)) holds A is_coarser_than ( rng g)

    proof

      let L be Semilattice, A be Subset of L, f,g be sequence of the carrier of L such that

       A1: ( rng f) = A and

       A2: for n be Element of NAT holds (g . n) = ( "/\" ({ (f . m) where m be Element of NAT : m <= n },L));

      let a be Element of L;

      assume a in A;

      then

      consider n be object such that

       A3: n in ( dom f) and

       A4: (f . n) = a by A1, FUNCT_1:def 3;

      reconsider n as Element of NAT by A3;

      reconsider T = { (f . m) where m be Element of NAT : m <= n } as non empty finite Subset of L by Lm1;

      take b = ( "/\" (T,L));

      ( dom g) = NAT & (g . n) = b by A2, FUNCT_2:def 1;

      hence b in ( rng g) by FUNCT_1:def 3;

      (f . n) in T;

      then

       A5: {(f . n)} c= T by ZFMISC_1: 31;

       ex_inf_of ( {(f . n)},L) & ex_inf_of (T,L) by YELLOW_0: 55;

      then b <= ( "/\" ( {(f . n)},L)) by A5, YELLOW_0: 35;

      hence b <= a by A4, YELLOW_0: 39;

    end;

    theorem :: WAYBEL12:32

    

     Th32: for L be Semilattice, F be Filter of L, G be GeneratorSet of F holds for f,g be sequence of the carrier of L st ( rng f) = G & for n be Element of NAT holds (g . n) = ( "/\" ({ (f . m) where m be Element of NAT : m <= n },L)) holds ( rng g) is GeneratorSet of F

    proof

      let L be Semilattice, F be Filter of L, G be GeneratorSet of F, f,g be sequence of the carrier of L such that

       A1: ( rng f) = G and

       A2: for n be Element of NAT holds (g . n) = ( "/\" ({ (f . m) where m be Element of NAT : m <= n },L));

      

       A3: ( rng g) is_coarser_than F

      proof

        let a be Element of L;

        assume a in ( rng g);

        then

        consider n be object such that

         A4: n in ( dom g) and

         A5: (g . n) = a by FUNCT_1:def 3;

        reconsider n as Element of NAT by A4;

        reconsider Y = { (f . m) where m be Element of NAT : m <= n } as non empty finite Subset of L by Lm1;

        

         A6: Y c= G

        proof

          let q be object;

          assume q in Y;

          then

           A7: ex m be Element of NAT st q = (f . m) & m <= n;

          ( dom f) = NAT by FUNCT_2:def 1;

          hence thesis by A1, A7, FUNCT_1:def 3;

        end;

        G c= F by Lm4;

        then Y c= F by A6;

        then

         A8: ( "/\" (Y,L)) in F by WAYBEL_0: 43;

        (g . n) = ( "/\" (Y,L)) by A2;

        hence ex b be Element of L st b in F & b <= a by A5, A8;

      end;

      (g . 0 ) in ( rng g) by FUNCT_2: 4;

      hence thesis by A1, A2, A3, Th30, Th31;

    end;

    begin

    theorem :: WAYBEL12:33

    

     Th33: for L be lower-bounded continuous LATTICE, V be Open upper Subset of L holds for F be Filter of L, v be Element of L st (V "/\" F) c= V & v in V & ex A be non empty GeneratorSet of F st A is countable holds ex O be Open Filter of L st O c= V & v in O & F c= O

    proof

      let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, F be Filter of L, v be Element of L such that

       A1: (V "/\" F) c= V and

       A2: v in V;

      reconsider V1 = V as non empty Open upper Subset of L by A2;

      reconsider v1 = v as Element of V1 by A2;

      reconsider G = { x where x be Element of L : (V "/\" {x}) c= V } as Filter of L by Th23, Th24, Th25;

      given A be non empty GeneratorSet of F such that

       A3: A is countable;

      consider f be sequence of A such that

       A4: ( rng f) = A by A3, CARD_3: 96;

      reconsider f as sequence of the carrier of L by FUNCT_2: 7;

      deffunc F( Element of NAT ) = ( "/\" ({ (f . m) where m be Element of NAT : m <= $1 },L));

      consider g be sequence of the carrier of L such that

       A5: for n be Element of NAT holds (g . n) = F(n) from FUNCT_2:sch 4;

      defpred P[ Nat, set, set] means ex x1,y1 be Element of V1, z1 be Element of L st x1 = $2 & y1 = $3 & z1 = (g . ($1 + 1)) & y1 << (x1 "/\" z1);

      

       A6: ( dom g) = NAT by FUNCT_2:def 1;

      then

      reconsider AA = ( rng g) as non empty Subset of L by RELAT_1: 42;

      

       A7: AA is GeneratorSet of F by A4, A5, Th32;

      

       A8: F c= G

      proof

        let q be object;

        assume

         A9: q in F;

        then

        reconsider s = q as Element of L;

        

         A10: (V "/\" {s}) = { (s "/\" t) where t be Element of L : t in V } by YELLOW_4: 42;

        (V "/\" {s}) c= V

        proof

          let w be object;

          assume w in (V "/\" {s});

          then

          consider t be Element of L such that

           A11: w = (s "/\" t) and

           A12: t in V by A10;

          (t "/\" s) in (V "/\" F) by A9, A12;

          hence thesis by A1, A11;

        end;

        hence thesis;

      end;

      

       A13: for n be Nat, x be Element of V1 holds ex y be Element of V1 st P[n, x, y]

      proof

        let n be Nat, x be Element of V1;

        AA c= F by A7, Lm4;

        then

         A14: AA c= G by A8;

        (g . (n + 1)) in AA by A6, FUNCT_1:def 3;

        then (g . (n + 1)) in G by A14;

        then

        consider g1 be Element of L such that

         A15: (g . (n + 1)) = g1 and

         A16: (V "/\" {g1}) c= V;

        g1 in {g1} by TARSKI:def 1;

        then (x "/\" g1) in (V "/\" {g1});

        then ex y1 be Element of L st y1 in V & y1 << (x "/\" g1) by A16, WAYBEL_6:def 1;

        hence thesis by A15;

      end;

      consider h be sequence of V1 such that

       A17: (h . 0 ) = v1 and

       A18: for n be Nat holds P[n, (h . n), (h . (n + 1))] from RECDEF_1:sch 2( A13);

      

       A19: ( dom h) = NAT by FUNCT_2:def 1;

      then

       A20: (h . 0 ) in ( rng h) by FUNCT_1:def 3;

      then

      reconsider R = ( rng h) as non empty Subset of L by XBOOLE_1: 1;

      set O = ( uparrow ( fininfs R));

      

       A21: R c= O by WAYBEL_0: 62;

      

       A22: for x,y be Element of L, n be Nat st (h . n) = x & (h . (n + 1)) = y holds y <= x

      proof

        let x,y be Element of L, n be Nat such that

         A23: (h . n) = x & (h . (n + 1)) = y;

        consider x1,y1 be Element of V1, z1 be Element of L such that

         A24: x1 = (h . n) & y1 = (h . (n + 1)) and z1 = (g . (n + 1)) and

         A25: y1 << (x1 "/\" z1) by A18;

        

         A26: (x1 "/\" z1) <= x1 by YELLOW_0: 23;

        y1 <= (x1 "/\" z1) by A25, WAYBEL_3: 1;

        hence thesis by A23, A24, A26, ORDERS_2: 3;

      end;

      

       A27: for x,y be Element of L, n,m be Element of NAT st (h . n) = x & (h . m) = y & n <= m holds y <= x

      proof

        defpred P[ Nat] means for a be Element of NAT , s,t be Element of L st t = (h . a) & s = (h . $1) & a <= $1 holds s <= t;

        

         A28: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A29: for j be Element of NAT , s,t be Element of L st t = (h . j) & s = (h . k) & j <= k holds s <= t;

          k in NAT by ORDINAL1:def 12;

          then (h . k) in R by A19, FUNCT_1:def 3;

          then

          reconsider s = (h . k) as Element of L;

          let a be Element of NAT , c,d be Element of L such that

           A30: d = (h . a) and

           A31: c = (h . (k + 1)) and

           A32: a <= (k + 1);

          

           A33: c <= s by A22, A31;

          per cases by A32, NAT_1: 8;

            suppose a <= k;

            then s <= d by A29, A30;

            hence thesis by A33, ORDERS_2: 3;

          end;

            suppose a = (k + 1);

            hence thesis by A30, A31;

          end;

        end;

        

         A34: P[ 0 ] by NAT_1: 3;

        

         A35: for k be Nat holds P[k] from NAT_1:sch 2( A34, A28);

        let x,y be Element of L, n,m be Element of NAT ;

        assume (h . n) = x & (h . m) = y & n <= m;

        hence thesis by A35;

      end;

      

       A36: for x,y be Element of L st x in R & y in R holds x <= y or y <= x

      proof

        let x,y be Element of L;

        assume that

         A37: x in R and

         A38: y in R;

        consider m be object such that

         A39: m in ( dom h) and

         A40: y = (h . m) by A38, FUNCT_1:def 3;

        reconsider m as Element of NAT by A39;

        consider n be object such that

         A41: n in ( dom h) and

         A42: x = (h . n) by A37, FUNCT_1:def 3;

        reconsider n as Element of NAT by A41;

        per cases ;

          suppose m <= n;

          hence thesis by A27, A42, A40;

        end;

          suppose n <= m;

          hence thesis by A27, A42, A40;

        end;

      end;

      

       A43: O is Open

      proof

        let x be Element of L;

        assume x in O;

        then

        consider y be Element of L such that

         A44: y <= x and

         A45: y in ( fininfs R) by WAYBEL_0:def 16;

        consider Y be finite Subset of R such that

         A46: y = ( "/\" (Y,L)) and ex_inf_of (Y,L) by A45;

        per cases ;

          suppose Y <> {} ;

          then y in Y by A36, A46, Th27;

          then

          consider n be object such that

           A47: n in ( dom h) and

           A48: (h . n) = y by FUNCT_1:def 3;

          reconsider n as Element of NAT by A47;

          consider x1,y1 be Element of V1, z1 be Element of L such that

           A49: x1 = (h . n) and

           A50: y1 = (h . (n + 1)) and z1 = (g . (n + 1)) and

           A51: y1 << (x1 "/\" z1) by A18;

          take y1;

          y1 in R by A19, A50, FUNCT_1:def 3;

          hence y1 in O by A21;

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

          then y1 << x1 by A51, WAYBEL_3: 2;

          hence thesis by A44, A48, A49, WAYBEL_3: 2;

        end;

          suppose

           A52: Y = {} ;

          consider b be object such that

           A53: b in R by XBOOLE_0:def 1;

          reconsider b as Element of L by A53;

          consider n be object such that

           A54: n in ( dom h) and (h . n) = b by A53, FUNCT_1:def 3;

          reconsider n as Element of NAT by A54;

          

           A55: x <= ( Top L) by YELLOW_0: 45;

          consider x1,y1 be Element of V1, z1 be Element of L such that x1 = (h . n) and

           A56: y1 = (h . (n + 1)) and z1 = (g . (n + 1)) and

           A57: y1 << (x1 "/\" z1) by A18;

          y = ( Top L) by A46, A52, YELLOW_0:def 12;

          then x = ( Top L) by A44, A55, ORDERS_2: 2;

          then

           A58: x1 <= x by YELLOW_0: 45;

          take y1;

          y1 in R by A19, A56, FUNCT_1:def 3;

          hence y1 in O by A21;

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

          then y1 << x1 by A57, WAYBEL_3: 2;

          hence thesis by A58, WAYBEL_3: 2;

        end;

      end;

      

       A59: for n be Element of NAT , a,b be Element of L st a = (g . n) & b = (g . (n + 1)) holds b <= a

      proof

        let n be Element of NAT , a,b be Element of L such that

         A60: a = (g . n) & b = (g . (n + 1));

        reconsider gn = { (f . m) where m be Element of NAT : m <= n }, gn1 = { (f . k) where k be Element of NAT : k <= (n + 1) } as non empty finite Subset of L by Lm1;

        

         A61: ex_inf_of (gn,L) & ex_inf_of (gn1,L) by YELLOW_0: 55;

        

         A62: gn c= gn1

        proof

          let i be object;

          assume i in gn;

          then

          consider k be Element of NAT such that

           A63: i = (f . k) and

           A64: k <= n;

          k <= (n + 1) by A64, NAT_1: 12;

          hence thesis by A63;

        end;

        a = ( "/\" (gn,L)) & b = ( "/\" (gn1,L)) by A5, A60;

        hence thesis by A61, A62, YELLOW_0: 35;

      end;

      

       A65: AA is_coarser_than R

      proof

        let a be Element of L;

        assume a in AA;

        then

        consider x be object such that

         A66: x in ( dom g) and

         A67: (g . x) = a by FUNCT_1:def 3;

        reconsider x as Element of NAT by A66;

        consider x1,y1 be Element of V1, z1 be Element of L such that x1 = (h . x) and

         A68: y1 = (h . (x + 1)) and

         A69: z1 = (g . (x + 1)) and

         A70: y1 << (x1 "/\" z1) by A18;

        (x1 "/\" z1) <= z1 & y1 <= (x1 "/\" z1) by A70, WAYBEL_3: 1, YELLOW_0: 23;

        then

         A71: y1 <= z1 by ORDERS_2: 3;

        

         A72: (h . (x + 1)) in R by A19, FUNCT_1:def 3;

        z1 <= a by A59, A67, A69;

        hence ex b be Element of L st b in R & b <= a by A68, A72, A71, ORDERS_2: 3;

      end;

      reconsider O as Open Filter of L by A43;

      R is_coarser_than O by A21, Th16;

      then

       A73: AA c= O by A65, YELLOW_4: 7, YELLOW_4: 8;

      take O;

      thus O c= V

      proof

        let q be object;

        assume q in O;

        then

        reconsider q as Element of O;

        consider y be Element of L such that

         A74: y <= q and

         A75: y in ( fininfs R) by WAYBEL_0:def 16;

        consider Y be finite Subset of R such that

         A76: y = ( "/\" (Y,L)) and ex_inf_of (Y,L) by A75;

        per cases ;

          suppose Y <> {} ;

          then y in Y by A36, A76, Th27;

          then

          consider n be object such that

           A77: n in ( dom h) and

           A78: (h . n) = y by FUNCT_1:def 3;

          reconsider n as Element of NAT by A77;

          ex x1,y1 be Element of V1, z1 be Element of L st x1 = (h . n) & y1 = (h . (n + 1)) & z1 = (g . (n + 1)) & y1 << (x1 "/\" z1) by A18;

          hence thesis by A74, A78, WAYBEL_0:def 20;

        end;

          suppose

           A79: Y = {} ;

          

           A80: q <= ( Top L) by YELLOW_0: 45;

          y = ( Top L) by A76, A79, YELLOW_0:def 12;

          then q = ( Top L) by A74, A80, ORDERS_2: 2;

          hence thesis by Th8;

        end;

      end;

      thus v in O by A17, A20, A21;

      ( uparrow ( fininfs AA)) = F by A7, Def3;

      hence thesis by A73, WAYBEL_0: 62;

    end;

    theorem :: WAYBEL12:34

    

     Th34: for L be lower-bounded continuous LATTICE, V be Open upper Subset of L holds for N be non empty countable Subset of L holds for v be Element of L st (V "/\" N) c= V & v in V holds ex O be Open Filter of L st ( {v} "/\" N) c= O & O c= V & v in O

    proof

      let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, N be non empty countable Subset of L, v be Element of L such that

       A1: (V "/\" N) c= V and

       A2: v in V;

      reconsider G = { x where x be Element of L : (V "/\" {x}) c= V } as Filter of L by Th23, Th24, Th25;

      

       A3: N c= G

      proof

        let q be object;

        assume

         A4: q in N;

        then

        reconsider q1 = q as Element of L;

        

         A5: ( {q1} "/\" V) = { (q1 "/\" y) where y be Element of L : y in V } by YELLOW_4: 42;

        (V "/\" {q1}) c= V

        proof

          let t be object;

          assume t in (V "/\" {q1});

          then

          consider y be Element of L such that

           A6: t = (q1 "/\" y) and

           A7: y in V by A5;

          (q1 "/\" y) in (N "/\" V) by A4, A7;

          hence thesis by A1, A6;

        end;

        hence thesis;

      end;

      N is GeneratorSet of ( uparrow ( fininfs N)) by Def3;

      then

      consider F be Filter of L such that

       A8: N is GeneratorSet of F;

      F = ( uparrow ( fininfs N)) by A8, Def3;

      then

       A9: F c= G by A3, WAYBEL_0: 62;

      (V "/\" F) c= V

      proof

        let q be object;

        assume q in (V "/\" F);

        then

        consider d,f be Element of L such that

         A10: q = (d "/\" f) and

         A11: d in V and

         A12: f in F;

        f in G by A9, A12;

        then

        consider x be Element of L such that

         A13: f = x and

         A14: (V "/\" {x}) c= V;

        x in {x} by TARSKI:def 1;

        then (d "/\" f) in (V "/\" {x}) by A11, A13;

        hence thesis by A10, A14;

      end;

      then

      consider O be Open Filter of L such that

       A15: O c= V and

       A16: v in O and

       A17: F c= O by A2, A8, Th33;

      take O;

      

       A18: ( {v} "/\" N) = { (v "/\" n) where n be Element of L : n in N } by YELLOW_4: 42;

      thus ( {v} "/\" N) c= O

      proof

        let q be object;

        assume q in ( {v} "/\" N);

        then

        consider n be Element of L such that

         A19: q = (v "/\" n) and

         A20: n in N by A18;

        N c= F by A8, Lm4;

        then N c= O by A17;

        then (v "/\" n) in (O "/\" O) by A16, A20;

        hence thesis by A19, Th21;

      end;

      thus thesis by A15, A16;

    end;

    theorem :: WAYBEL12:35

    

     Th35: for L be lower-bounded continuous LATTICE, V be Open upper Subset of L holds for N be non empty countable Subset of L, x,y be Element of L st (V "/\" N) c= V & y in V & not x in V holds ex p be irreducible Element of L st x <= p & not p in ( uparrow ( {y} "/\" N))

    proof

      let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, N be non empty countable Subset of L, x,y be Element of L such that

       A1: (V "/\" N) c= V & y in V and

       A2: not x in V;

      consider O be Open Filter of L such that

       A3: ( {y} "/\" N) c= O and

       A4: O c= V and y in O by A1, Th34;

      ( uparrow O) c= O & O c= ( uparrow O) by WAYBEL_0: 16, WAYBEL_0: 24;

      then ( uparrow O) = O;

      then

       A5: ( uparrow ( {y} "/\" N)) c= O by A3, YELLOW_3: 7;

       not x in O by A2, A4;

      then x in (O ` ) by XBOOLE_0:def 5;

      then

      consider p be Element of L such that

       A6: x <= p and

       A7: p is_maximal_in (O ` ) by WAYBEL_6: 9;

      reconsider p as irreducible Element of L by A7, WAYBEL_6: 13;

      take p;

      thus x <= p by A6;

      p in (O ` ) by A7, WAYBEL_4: 55;

      hence thesis by A5, XBOOLE_0:def 5;

    end;

    theorem :: WAYBEL12:36

    

     Th36: for L be lower-bounded continuous LATTICE, x be Element of L holds for N be non empty countable Subset of L st for n,y be Element of L st not y <= x & n in N holds not (y "/\" n) <= x holds for y be Element of L st not y <= x holds ex p be irreducible Element of L st x <= p & not p in ( uparrow ( {y} "/\" N))

    proof

      let L be lower-bounded continuous LATTICE, x be Element of L, N be non empty countable Subset of L such that

       A1: for n,y be Element of L st not y <= x & n in N holds not (y "/\" n) <= x;

      set V = (( downarrow x) ` );

      

       A2: (V "/\" N) c= V

      proof

        let q be object;

        assume q in (V "/\" N);

        then

        consider v,n be Element of L such that

         A3: q = (v "/\" n) and

         A4: v in V and

         A5: n in N;

         not v in ( downarrow x) by A4, XBOOLE_0:def 5;

        then not v <= x by WAYBEL_0: 17;

        then not (v "/\" n) <= x by A1, A5;

        then not (v "/\" n) in ( downarrow x) by WAYBEL_0: 17;

        hence thesis by A3, XBOOLE_0:def 5;

      end;

      x <= x;

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

      then

       A6: not x in V by XBOOLE_0:def 5;

      let y be Element of L;

      assume not y <= x;

      then not y in ( downarrow x) by WAYBEL_0: 17;

      then y in V by XBOOLE_0:def 5;

      hence thesis by A2, A6, Th35;

    end;

    definition

      let L be non empty RelStr, u be Element of L;

      :: WAYBEL12:def4

      attr u is dense means for v be Element of L st v <> ( Bottom L) holds (u "/\" v) <> ( Bottom L);

    end

    registration

      let L be upper-bounded Semilattice;

      cluster ( Top L) -> dense;

      coherence by WAYBEL_1: 4;

    end

    registration

      let L be upper-bounded Semilattice;

      cluster dense for Element of L;

      existence

      proof

        take ( Top L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL12:37

    for L be non trivial bounded Semilattice holds for x be Element of L st x is dense holds x <> ( Bottom L)

    proof

      let L be non trivial bounded Semilattice, x be Element of L such that

       A1: x is dense;

      ( Top L) <> ( Bottom L) by WAYBEL_7: 3;

      then (x "/\" ( Top L)) <> ( Bottom L) by A1;

      hence thesis by WAYBEL_1: 4;

    end;

    definition

      let L be non empty RelStr, D be Subset of L;

      :: WAYBEL12:def5

      attr D is dense means

      : Def5: for d be Element of L st d in D holds d is dense;

    end

    theorem :: WAYBEL12:38

    

     Th38: for L be upper-bounded Semilattice holds {( Top L)} is dense by TARSKI:def 1;

    registration

      let L be upper-bounded Semilattice;

      cluster non empty finite countable dense for Subset of L;

      existence

      proof

        take {( Top L)};

        thus {( Top L)} is non empty finite countable;

        thus thesis by Th38;

      end;

    end

    ::$Notion-Name

    theorem :: WAYBEL12:39

    

     Th39: for L be lower-bounded continuous LATTICE holds for D be non empty countable dense Subset of L, u be Element of L st u <> ( Bottom L) holds ex p be irreducible Element of L st p <> ( Top L) & not p in ( uparrow ( {u} "/\" D))

    proof

      let L be lower-bounded continuous LATTICE, D be non empty countable dense Subset of L, u be Element of L such that

       A1: u <> ( Bottom L);

      

       A2: for d,y be Element of L st not y <= ( Bottom L) & d in D holds not (y "/\" d) <= ( Bottom L)

      proof

        let d,y be Element of L such that

         A3: not y <= ( Bottom L);

        assume d in D;

        then d is dense by Def5;

        then

         A4: (y "/\" d) <> ( Bottom L) by A3;

        ( Bottom L) <= (y "/\" d) by YELLOW_0: 44;

        hence thesis by A4, ORDERS_2: 2;

      end;

      ( Bottom L) <= u by YELLOW_0: 44;

      then not u <= ( Bottom L) by A1, ORDERS_2: 2;

      then

      consider p be irreducible Element of L such that ( Bottom L) <= p and

       A5: not p in ( uparrow ( {u} "/\" D)) by A2, Th36;

      take p;

      thus p <> ( Top L) by A5, Th9;

      thus thesis by A5;

    end;

    theorem :: WAYBEL12:40

    

     Th40: for T be non empty TopSpace holds for A be Element of ( InclPoset the topology of T) holds for B be Subset of T st A = B & (B ` ) is irreducible holds A is irreducible

    proof

      let T be non empty TopSpace, A be Element of ( InclPoset the topology of T), B be Subset of T such that

       A1: A = B;

      assume that (B ` ) is non empty closed and

       A2: for S1,S2 be Subset of T st S1 is closed & S2 is closed & (B ` ) = (S1 \/ S2) holds S1 = (B ` ) or S2 = (B ` );

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

       A3: A = (x "/\" y);

      

       A4: 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 x1 = x, y1 = y as Subset of T;

      

       A5: y1 is open by A4;

      then

       A6: (y1 ` ) is closed;

      

       A7: x1 is open by A4;

      then (x1 /\ y1) is open by A5;

      then (x /\ y) in the topology of T;

      then A = (x /\ y) by A3, YELLOW_1: 9;

      then

       A8: (B ` ) = ((x1 ` ) \/ (y1 ` )) by A1, XBOOLE_1: 54;

      (x1 ` ) is closed by A7;

      then (x1 ` ) = (B ` ) or (y1 ` ) = (B ` ) by A2, A6, A8;

      hence thesis by A1, TOPS_1: 1;

    end;

    theorem :: WAYBEL12:41

    

     Th41: for T be non empty TopSpace holds for A be Element of ( InclPoset the topology of T) holds for B be Subset of T st A = B & A <> ( Top ( InclPoset the topology of T)) holds A is irreducible iff (B ` ) is irreducible

    proof

      let T be non empty TopSpace, A be Element of ( InclPoset the topology of T), B be Subset of T such that

       A1: A = B and

       A2: A <> ( Top ( InclPoset the topology of T));

      

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

      hereby

        assume

         A4: A is irreducible;

        thus (B ` ) is irreducible

        proof

          B <> the carrier of T by A1, A2, YELLOW_1: 24;

          then (the carrier of T \ B) <> {} by XBOOLE_1: 37;

          hence (B ` ) is non empty;

          ((B ` ) ` ) is open by A1, A3;

          hence (B ` ) is closed;

          let S1,S2 be Subset of T such that

           A5: S1 is closed & S2 is closed and

           A6: (B ` ) = (S1 \/ S2);

          

           A7: (S1 ` ) is open & (S2 ` ) is open by A5;

          then

          reconsider s1 = (S1 ` ), s2 = (S2 ` ) as Element of ( InclPoset the topology of T) by A3;

          ((S1 ` ) /\ (S2 ` )) is open by A7;

          then

           A8: (s1 /\ s2) in the topology of T;

          B = ((S1 \/ S2) ` ) by A6

          .= ((S1 ` ) /\ (S2 ` )) by XBOOLE_1: 53;

          then A = (s1 "/\" s2) by A1, A8, YELLOW_1: 9;

          then A = s1 or A = s2 by A4;

          hence thesis by A1;

        end;

      end;

      thus thesis by A1, Th40;

    end;

    theorem :: WAYBEL12:42

    

     Th42: for T be non empty TopSpace holds for A be Element of ( InclPoset the topology of T) holds for B be Subset of T st A = B holds A is dense iff B is everywhere_dense

    proof

      let T be non empty TopSpace, A be Element of ( InclPoset the topology of T), B be Subset of T such that

       A1: A = B;

      

       A2: ( Bottom ( InclPoset the topology of T)) = {} by PRE_TOPC: 1, YELLOW_1: 13;

      

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

      then

       A4: B is open by A1;

      hereby

        assume

         A5: A is dense;

        for Q be Subset of T st Q <> {} & Q is open holds B meets Q

        proof

          let Q be Subset of T such that

           A6: Q <> {} and

           A7: Q is open;

          reconsider q = Q as Element of ( InclPoset the topology of T) by A3, A7;

          (B /\ Q) is open by A4, A7;

          then

           A8: (A /\ q) in the topology of T by A1;

          (A "/\" q) <> ( Bottom ( InclPoset the topology of T)) by A2, A5, A6;

          then (B /\ Q) <> {} by A1, A2, A8, YELLOW_1: 9;

          hence thesis;

        end;

        then B is dense by TOPS_1: 45;

        hence B is everywhere_dense by A4, TOPS_3: 36;

      end;

      assume B is everywhere_dense;

      then

       A9: B is dense by TOPS_3: 33;

      let v be Element of ( InclPoset the topology of T) such that

       A10: v <> ( Bottom ( InclPoset the topology of T));

      v in the topology of T by A3;

      then

      reconsider V = v as Subset of T;

      

       A11: V is open by A3;

      B is open by A1, A3;

      then (B /\ V) is open by A11;

      then

       A12: (B /\ V) in the topology of T;

      B meets V by A2, A9, A10, A11, TOPS_1: 45;

      then (B /\ V) <> {} ;

      hence (A "/\" v) <> ( Bottom ( InclPoset the topology of T)) by A1, A2, A12, YELLOW_1: 9;

    end;

    theorem :: WAYBEL12:43

    

     Th43: for T be non empty TopSpace st T is locally-compact holds for D be countable Subset-Family of T st D is non empty dense open holds for O be non empty Subset of T st O is open holds ex A be irreducible Subset of T st for V be Subset of T st V in D holds (A /\ O) meets V

    proof

      let T be non empty TopSpace;

      assume T is locally-compact;

      then

      reconsider L = ( InclPoset the topology of T) as bounded continuous LATTICE by WAYBEL_3: 42;

      

       A1: the carrier of L = the topology of T by YELLOW_1: 1;

      let D be countable Subset-Family of T such that

       A2: D is non empty dense open;

      consider I be object such that

       A3: I in D by A2;

      reconsider I as Subset of T by A3;

      I is open by A2, A3;

      then

      reconsider i = I as Element of L by A1;

      set D1 = { d where d be Element of L : ex d1 be Subset of T st d1 in D & d1 = d & d is dense };

      D1 c= the carrier of L

      proof

        let q be object;

        assume q in D1;

        then ex d be Element of L st q = d & ex d1 be Subset of T st d1 in D & d1 = d & d is dense;

        hence thesis;

      end;

      then

      reconsider D1 as Subset of L;

      

       A4: D1 c= D

      proof

        let q be object;

        assume q in D1;

        then ex d be Element of L st q = d & ex d1 be Subset of T st d1 in D & d1 = d & d is dense;

        hence thesis;

      end;

      

       A5: D1 is dense

      proof

        let q be Element of L;

        assume q in D1;

        then ex d be Element of L st q = d & ex d1 be Subset of T st d1 in D & d1 = d & d is dense;

        hence thesis;

      end;

      let O be non empty Subset of T such that

       A6: O is open;

      reconsider u = O as Element of L by A6, A1;

      I is open dense by A2, A3;

      then I is everywhere_dense by TOPS_3: 36;

      then i is dense by Th42;

      then u <> ( Bottom L) & i in D1 by A3, PRE_TOPC: 1, YELLOW_1: 13;

      then

      consider p be irreducible Element of L such that

       A7: p <> ( Top L) and

       A8: not p in ( uparrow ( {u} "/\" D1)) by A4, A5, Th39;

      p in the topology of T by A1;

      then

      reconsider P = p as Subset of T;

      reconsider A = (P ` ) as irreducible Subset of T by A7, Th41;

      take A;

      let V be Subset of T;

      assume

       A9: V in D;

      then

       A10: V is open by A2;

      then

      reconsider v = V as Element of L by A1;

      

       A11: for d1 be Element of L st d1 in D1 holds not (u "/\" d1) <= p

      proof

        

         A12: u in {u} by TARSKI:def 1;

        let d1 be Element of L;

        assume d1 in D1;

        then (u "/\" d1) in ( {u} "/\" D1) by A12;

        hence thesis by A8, WAYBEL_0:def 16;

      end;

      V is dense by A2, A9;

      then V is everywhere_dense by A10, TOPS_3: 36;

      then v is dense by Th42;

      then v in D1 by A9;

      then not (u "/\" v) <= p by A11;

      then

       A13: not (u "/\" v) c= p by YELLOW_1: 3;

      (O /\ V) is open by A6, A10;

      then (u /\ v) in the topology of T;

      then not (O /\ V) c= p by A13, YELLOW_1: 9;

      then

      consider x be object such that

       A14: x in (O /\ V) and

       A15: not x in (A ` );

      reconsider x as Element of T by A14;

      x in A by A15, XBOOLE_0:def 5;

      then ((O /\ V) /\ A) <> {} by A14, XBOOLE_0:def 4;

      hence ((A /\ O) /\ V) <> {} by XBOOLE_1: 16;

    end;

    definition

      let T be non empty TopSpace;

      :: original: Baire

      redefine

      :: WAYBEL12:def6

      attr T is Baire means for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is open dense holds ex I be Subset of T st I = ( Intersect F) & I is dense;

      compatibility

      proof

        set D = ( bool the carrier of T);

        hereby

          assume

           A1: T is Baire;

          thus for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is open dense holds ex I be Subset of T st I = ( Intersect F) & I is dense

          proof

            let F be Subset-Family of T such that

             A2: F is countable and

             A3: for S be Subset of T st S in F holds S is open dense;

            for S be Subset of T st S in F holds S is everywhere_dense

            proof

              let S be Subset of T;

              assume S in F;

              then S is open dense by A3;

              hence thesis by TOPS_3: 36;

            end;

            hence thesis by A1, A2;

          end;

        end;

        assume

         A4: for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is open dense holds ex I be Subset of T st I = ( Intersect F) & I is dense;

        deffunc F( Element of D) = ( Int $1);

        let F be Subset-Family of T such that

         A5: F is countable and

         A6: for S be Subset of T st S in F holds S is everywhere_dense;

        set F1 = { ( Int A) where A be Subset of T : A in F };

        consider f be Function of D, D such that

         A7: for x be Element of D holds (f . x) = F(x) from FUNCT_2:sch 4;

        F1 c= (f .: F)

        proof

          let q be object;

          assume q in F1;

          then

          consider A be Subset of T such that

           A8: q = ( Int A) & A in F;

          ( dom f) = D & (f . A) = ( Int A) by A7, FUNCT_2:def 1;

          hence thesis by A8, FUNCT_1:def 6;

        end;

        then ( card F1) c= ( card F) by CARD_1: 66;

        then

         A9: F1 is countable by A5, Th1;

        reconsider J = ( Intersect F) as Subset of T;

        

         A10: F1 c= ( bool the carrier of T)

        proof

          let q be object;

          assume q in F1;

          then ex A be Subset of T st q = ( Int A) & A in F;

          hence thesis;

        end;

        take J;

        thus J = ( Intersect F);

        reconsider F1 as Subset-Family of T by A10;

        for X be set st X in F holds ( Intersect F1) c= X

        proof

          let X be set such that

           A11: X in F;

          reconsider X1 = X as Subset of T by A11;

          

           A12: ( Int X1) in F1 by A11;

          let q be object;

          assume q in ( Intersect F1);

          then ( Int X1) c= X1 & q in ( Int X1) by A12, SETFAM_1: 43, TOPS_1: 16;

          hence thesis;

        end;

        then

         A13: ( Intersect F1) c= ( Intersect F) by MSSUBFAM: 4;

        now

          let S be Subset of T;

          assume S in F1;

          then

          consider A be Subset of T such that

           A14: S = ( Int A) and

           A15: A in F;

          A is everywhere_dense by A6, A15;

          hence S is open dense by A14, TOPS_3: 35;

        end;

        then ex I be Subset of T st I = ( Intersect F1) & I is dense by A4, A9;

        hence thesis by A13, TOPS_1: 44;

      end;

    end

    theorem :: WAYBEL12:44

    for T be non empty TopSpace st T is sober locally-compact holds T is Baire

    proof

      let T be non empty TopSpace such that

       A1: T is sober locally-compact;

      let F be Subset-Family of T such that

       A2: F is countable and

       A3: for S be Subset of T st S in F holds S is open dense;

      

       A4: F is open by A3;

      for X be Subset of T st X in F holds X is dense by A3;

      then

       A5: F is open dense by A4;

      reconsider I = ( Intersect F) as Subset of T;

      take I;

      thus I = ( Intersect F);

      per cases ;

        suppose

         A6: F <> {} ;

        for Q be Subset of T st Q <> {} & Q is open holds ( Intersect F) meets Q

        proof

          let Q be Subset of T;

          assume that

           A7: Q <> {} and

           A8: Q is open;

          consider S be irreducible Subset of T such that

           A9: for V be Subset of T st V in F holds (S /\ Q) meets V by A1, A2, A5, A6, A7, A8, Th43;

          consider p be Point of T such that

           A10: p is_dense_point_of S and for q be Point of T st q is_dense_point_of S holds p = q by A1;

          S is closed by YELLOW_8:def 3;

          then

           A11: S = ( Cl {p}) by A10, YELLOW_8: 16;

          

           A12: for Y be set holds Y in F implies p in Y & p in Q

          proof

            let Y be set;

            assume

             A13: Y in F;

            then

            reconsider Y1 = Y as Subset of T;

            (S /\ Q) meets Y1 by A9, A13;

            then

             A14: ((S /\ Q) /\ Y1) <> {} ;

            now

              assume not p in (Q /\ Y1);

              then p in ((Q /\ Y1) ` ) by XBOOLE_0:def 5;

              then {p} c= ((Q /\ Y1) ` ) by ZFMISC_1: 31;

              then

               A15: ( Cl {p}) c= ( Cl ((Q /\ Y1) ` )) by PRE_TOPC: 19;

              Y1 is open by A3, A13;

              then (Q /\ Y1) is open by A8;

              then ((Q /\ Y1) ` ) is closed;

              then S c= ((Q /\ Y1) ` ) by A11, A15, PRE_TOPC: 22;

              then S misses (Q /\ Y1) by SUBSET_1: 23;

              then (S /\ (Q /\ Y1)) = {} ;

              hence contradiction by A14, XBOOLE_1: 16;

            end;

            hence thesis by XBOOLE_0:def 4;

          end;

          then for Y be set holds Y in F implies p in Y;

          then

           A16: p in ( Intersect F) by SETFAM_1: 43;

          ex Y be object st Y in F by A6, XBOOLE_0:def 1;

          then p in Q by A12;

          then (( Intersect F) /\ Q) <> {} by A16, XBOOLE_0:def 4;

          hence thesis;

        end;

        hence thesis by TOPS_1: 45;

      end;

        suppose F = {} ;

        then ( Intersect F) = ( [#] T) by SETFAM_1:def 9;

        hence thesis;

      end;

    end;