waybel_3.miz



    begin

    definition

      let L be non empty reflexive RelStr;

      let x,y be Element of L;

      :: WAYBEL_3:def1

      pred x is_way_below y means for D be non empty directed Subset of L st y <= ( sup D) holds ex d be Element of L st d in D & x <= d;

    end

    notation

      let L be non empty reflexive RelStr;

      let x,y be Element of L;

      synonym x << y for x is_way_below y;

      synonym y >> x for x is_way_below y;

    end

    definition

      let L be non empty reflexive RelStr;

      let x be Element of L;

      :: WAYBEL_3:def2

      attr x is compact means x is_way_below x;

    end

    notation

      let L be non empty reflexive RelStr;

      let x be Element of L;

      synonym x is isolated_from_below for x is compact;

    end

    theorem :: WAYBEL_3:1

    

     Th1: for L be non empty reflexive antisymmetric RelStr holds for x,y be Element of L st x << y holds x <= y

    proof

      let L be non empty reflexive antisymmetric RelStr;

      let x,y be Element of L such that

       A1: for D be non empty directed Subset of L st y <= ( sup D) holds ex d be Element of L st d in D & x <= d;

      

       A2: {y} is directed by WAYBEL_0: 5;

      ( sup {y}) = y by YELLOW_0: 39;

      then ex d be Element of L st (d in {y}) & (x <= d) by A1, A2;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: WAYBEL_3:2

    

     Th2: for L be non empty reflexive transitive RelStr, u,x,y,z be Element of L st u <= x & x << y & y <= z holds u << z

    proof

      let L be non empty reflexive transitive RelStr;

      let u,x,y,z be Element of L such that

       A1: u <= x and

       A2: for D be non empty directed Subset of L st y <= ( sup D) holds ex d be Element of L st d in D & x <= d and

       A3: y <= z;

      let D be non empty directed Subset of L;

      assume z <= ( sup D);

      then y <= ( sup D) by A3, ORDERS_2: 3;

      then

      consider d be Element of L such that

       A4: d in D and

       A5: x <= d by A2;

      take d;

      thus thesis by A1, A4, A5, ORDERS_2: 3;

    end;

    theorem :: WAYBEL_3:3

    

     Th3: for L be non empty Poset st L is with_suprema or L is /\-complete holds for x,y,z be Element of L st x << z & y << z holds ex_sup_of ( {x, y},L) & (x "\/" y) << z

    proof

      let L be non empty Poset such that

       A1: L is with_suprema or L is /\-complete;

      let x,y,z be Element of L;

      assume

       A2: z >> x;

      then

       A3: z >= x by Th1;

      assume

       A4: z >> y;

      then

       A5: z >= y by Th1;

      now

        per cases by A1;

          suppose L is with_suprema;

          hence ex_sup_of ( {x, y},L) by YELLOW_0: 20;

        end;

          suppose

           A7: L is /\-complete;

          set X = { a where a be Element of L : a >= x & a >= y };

          X c= the carrier of L

          proof

            let a be object;

            assume a in X;

            then ex z be Element of L st a = z & z >= x & z >= y;

            hence thesis;

          end;

          then

          reconsider X as Subset of L;

          z in X by A3, A5;

          then ex_inf_of (X,L) by A7, WAYBEL_0: 76;

          then

          consider c be Element of L such that

           A8: c is_<=_than X and

           A9: for d be Element of L st d is_<=_than X holds d <= c;

          

           A10: c is_>=_than {x, y}

          proof

            let a be Element of L;

            assume

             A11: a in {x, y};

            a is_<=_than X

            proof

              let b be Element of L;

              assume b in X;

              then ex z be Element of L st b = z & z >= x & z >= y;

              hence thesis by A11, TARSKI:def 2;

            end;

            hence thesis by A9;

          end;

          now

            let a be Element of L;

            assume

             A12: a is_>=_than {x, y};

            then

             A13: a >= x by YELLOW_0: 8;

            a >= y by A12, YELLOW_0: 8;

            then a in X by A13;

            hence c <= a by A8;

          end;

          hence ex_sup_of ( {x, y},L) by A10, YELLOW_0: 15;

        end;

      end;

      let D be non empty directed Subset of L;

      assume

       A14: z <= ( sup D);

      then

      consider d1 be Element of L such that

       A15: d1 in D and

       A16: x <= d1 by A2;

      consider d2 be Element of L such that

       A17: d2 in D and

       A18: y <= d2 by A4, A14;

      consider d be Element of L such that

       A19: d in D and

       A20: d1 <= d and

       A21: d2 <= d by A15, A17, WAYBEL_0:def 1;

      

       A22: x <= d by A16, A20, ORDERS_2: 3;

      

       A23: y <= d by A18, A21, ORDERS_2: 3;

      take d;

      thus thesis by A6, A19, A22, A23, YELLOW_0: 18;

    end;

    theorem :: WAYBEL_3:4

    

     Th4: for L be lower-bounded antisymmetric reflexive non empty RelStr holds for x be Element of L holds ( Bottom L) << x

    proof

      let L be lower-bounded antisymmetric reflexive non empty RelStr;

      let x be Element of L;

      let D be non empty directed Subset of L;

      assume x <= ( sup D);

      set d = the Element of D;

      reconsider d as Element of L;

      take d;

      thus thesis by YELLOW_0: 44;

    end;

    theorem :: WAYBEL_3:5

    for L be non empty Poset, x,y,z be Element of L st x << y & y << z holds x << z

    proof

      let L be non empty Poset, x,y,z be Element of L;

      assume x << y;

      then x <= y by Th1;

      hence thesis by Th2;

    end;

    theorem :: WAYBEL_3:6

    for L be non empty reflexive antisymmetric RelStr, x,y be Element of L st x << y & x >> y holds x = y

    proof

      let L be non empty reflexive antisymmetric RelStr, x,y be Element of L;

      assume that

       A1: x << y and

       A2: x >> y;

      

       A3: x <= y by A1, Th1;

      y <= x by A2, Th1;

      hence thesis by A3, ORDERS_2: 2;

    end;

    definition

      let L be non empty reflexive RelStr;

      let x be Element of L;

      

       A1: { y where y be Element of L : y << x } c= the carrier of L

      proof

        let z be object;

        assume z in { y where y be Element of L : y << x };

        then ex y be Element of L st z = y & y << x;

        hence thesis;

      end;

      :: WAYBEL_3:def3

      func waybelow x -> Subset of L equals { y where y be Element of L : y << x };

      correctness by A1;

      

       A2: { y where y be Element of L : y >> x } c= the carrier of L

      proof

        let z be object;

        assume z in { y where y be Element of L : y >> x };

        then ex y be Element of L st z = y & y >> x;

        hence thesis;

      end;

      :: WAYBEL_3:def4

      func wayabove x -> Subset of L equals { y where y be Element of L : y >> x };

      correctness by A2;

    end

    theorem :: WAYBEL_3:7

    

     Th7: for L be non empty reflexive RelStr, x,y be Element of L holds x in ( waybelow y) iff x << y

    proof

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

      x in ( waybelow y) iff ex z be Element of L st x = z & z << y;

      hence thesis;

    end;

    theorem :: WAYBEL_3:8

    

     Th8: for L be non empty reflexive RelStr, x,y be Element of L holds x in ( wayabove y) iff x >> y

    proof

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

      x in ( wayabove y) iff ex z be Element of L st x = z & z >> y;

      hence thesis;

    end;

    theorem :: WAYBEL_3:9

    

     Th9: for L be non empty reflexive antisymmetric RelStr holds for x be Element of L holds x is_>=_than ( waybelow x) by Th7, Th1;

    theorem :: WAYBEL_3:10

    for L be non empty reflexive antisymmetric RelStr holds for x be Element of L holds x is_<=_than ( wayabove x) by Th8, Th1;

    theorem :: WAYBEL_3:11

    

     Th11: for L be non empty reflexive antisymmetric RelStr holds for x be Element of L holds ( waybelow x) c= ( downarrow x) & ( wayabove x) c= ( uparrow x)

    proof

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

      hereby

        let a be object;

        assume a in ( waybelow x);

        then

        consider y be Element of L such that

         A1: a = y and

         A2: y << x;

        y <= x by A2, Th1;

        hence a in ( downarrow x) by A1, WAYBEL_0: 17;

      end;

      let a be object;

      assume a in ( wayabove x);

      then

      consider y be Element of L such that

       A3: a = y and

       A4: y >> x;

      x <= y by A4, Th1;

      hence thesis by A3, WAYBEL_0: 18;

    end;

    theorem :: WAYBEL_3:12

    

     Th12: for L be non empty reflexive transitive RelStr holds for x,y be Element of L st x <= y holds ( waybelow x) c= ( waybelow y) & ( wayabove y) c= ( wayabove x)

    proof

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

      assume

       A1: x <= y;

      hereby

        let z be object;

        assume z in ( waybelow x);

        then

        consider v be Element of L such that

         A2: z = v and

         A3: v << x;

        v << y by A1, A3, Th2;

        hence z in ( waybelow y) by A2;

      end;

      let z be object;

      assume z in ( wayabove y);

      then

      consider v be Element of L such that

       A4: z = v and

       A5: v >> y;

      v >> x by A1, A5, Th2;

      hence thesis by A4;

    end;

    registration

      let L be lower-bounded non empty reflexive antisymmetric RelStr;

      let x be Element of L;

      cluster ( waybelow x) -> non empty;

      coherence

      proof

        ( Bottom L) << x by Th4;

        hence thesis by Th7;

      end;

    end

    registration

      let L be non empty reflexive transitive RelStr;

      let x be Element of L;

      cluster ( waybelow x) -> lower;

      coherence

      proof

        let z,y be Element of L;

        assume z in ( waybelow x);

        then z << x by Th7;

        then y <= z implies y << x by Th2;

        hence y <= z implies y in ( waybelow x);

      end;

      cluster ( wayabove x) -> upper;

      coherence

      proof

        hereby

          let z,y be Element of L;

          assume z in ( wayabove x);

          then z >> x by Th8;

          then y >= z implies y >> x by Th2;

          hence y >= z implies y in ( wayabove x);

        end;

      end;

    end

    registration

      let L be sup-Semilattice;

      let x be Element of L;

      cluster ( waybelow x) -> directed;

      coherence

      proof

        let v,y be Element of L;

        assume that

         A1: v in ( waybelow x) and

         A2: y in ( waybelow x);

        

         A3: v << x by A1, Th7;

        

         A4: y << x by A2, Th7;

        then

         A5: ex_sup_of ( {v, y},L) by A3, Th3;

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

        z << x by A3, A4, Th3;

        hence z in ( waybelow x);

        thus v <= z & y <= z by A5, YELLOW_0: 18;

      end;

    end

    registration

      let L be /\-complete non empty Poset;

      let x be Element of L;

      cluster ( waybelow x) -> directed;

      coherence

      proof

        let v,y be Element of L;

        assume that

         A1: v in ( waybelow x) and

         A2: y in ( waybelow x);

        

         A3: v << x by A1, Th7;

        

         A4: y << x by A2, Th7;

        then

         A5: ex_sup_of ( {v, y},L) by A3, Th3;

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

        z << x by A3, A4, Th3;

        hence z in ( waybelow x);

        thus v <= z & y <= z by A5, YELLOW_0: 18;

      end;

    end

    registration

      let L be connected non empty RelStr;

      cluster -> directed filtered for Subset of L;

      coherence

      proof

        let X be Subset of L;

        thus X is directed

        proof

          let x,y be Element of L;

          x <= y & y <= y or x >= x & x >= y by WAYBEL_0:def 29;

          hence thesis;

        end;

        let x,y be Element of L;

        x >= y & y <= y or x >= x & x <= y by WAYBEL_0:def 29;

        hence thesis;

      end;

    end

    registration

      cluster up-complete lower-bounded -> complete for non empty Chain;

      coherence

      proof

        let L be non empty Chain such that

         A1: L is up-complete lower-bounded;

        now

          let X be Subset of L;

          X = {} or X <> {} ;

          hence ex_sup_of (X,L) by A1, WAYBEL_0: 75, YELLOW_0: 42;

        end;

        hence thesis by YELLOW_0: 53;

      end;

    end

    registration

      cluster complete for non empty Chain;

      existence

      proof

        set x = the set, O = the Order of {x};

         RelStr (# {x}, O #) is 1 -element RelStr;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_3:13

    

     Th13: for L be up-complete non empty Chain holds for x,y be Element of L st x < y holds x << y

    proof

      let L be up-complete Chain, x,y be Element of L such that

       A1: x <= y and

       A2: x <> y;

      let D be non empty directed Subset of L such that

       A3: y <= ( sup D) and

       A4: for d be Element of L st d in D holds not x <= d;

      

       A5: ex_sup_of (D,L) by WAYBEL_0: 75;

      x is_>=_than D

      proof

        let z be Element of L;

        assume z in D;

        then not x <= z by A4;

        hence thesis by WAYBEL_0:def 29;

      end;

      then x >= ( sup D) by A5, YELLOW_0:def 9;

      then x >= y by A3, ORDERS_2: 3;

      hence contradiction by A1, A2, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_3:14

    for L be non empty reflexive antisymmetric RelStr holds for x,y be Element of L st not x is compact & x << y holds x < y by Th1;

    theorem :: WAYBEL_3:15

    for L be non empty lower-bounded reflexive antisymmetric RelStr holds ( Bottom L) is compact by Th4;

    theorem :: WAYBEL_3:16

    

     Th16: for L be up-complete non empty Poset holds for D be non empty finite directed Subset of L holds ( sup D) in D

    proof

      let L be up-complete non empty Poset;

      let D be non empty finite directed Subset of L;

      D c= D;

      then

      consider d be Element of L such that

       A1: d in D and

       A2: d is_>=_than D by WAYBEL_0: 1;

      

       A3: ex_sup_of (D,L) by WAYBEL_0: 75;

      then

       A4: ( sup D) is_>=_than D by YELLOW_0: 30;

      

       A5: ( sup D) <= d by A2, A3, YELLOW_0: 30;

      ( sup D) >= d by A1, A4;

      hence thesis by A1, A5, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_3:17

    for L be up-complete non empty Poset st L is finite holds for x be Element of L holds x is isolated_from_below

    proof

      let L be up-complete non empty Poset such that

       A1: the carrier of L is finite;

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

      assume x <= ( sup D);

      hence thesis by A1, Th16;

    end;

    begin

    theorem :: WAYBEL_3:18

    

     Th18: for L be complete LATTICE, x,y be Element of L st x << y holds for X be Subset of L st y <= ( sup X) holds ex A be finite Subset of L st A c= X & x <= ( sup A)

    proof

      let L be complete LATTICE, x,y be Element of L;

      assume

       A1: x << y;

      let X be Subset of L;

      assume

       A2: y <= ( sup X);

      defpred P[ set] means ex Y be finite Subset of X st ex_sup_of (Y,L) & $1 = ( "\/" (Y,L));

      consider F be Subset of L such that

       A3: for a be Element of L holds a in F iff P[a] from SUBSET_1:sch 3;

      

       A4: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F by A3, YELLOW_0: 17;

      

       A5: for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L) by YELLOW_0: 17;

      

       A6: {} c= X;

       ex_sup_of ( {} ,L) by YELLOW_0: 17;

      then ( "\/" ( {} ,L)) in F by A3, A6;

      then

      reconsider F as directed non empty Subset of L by A3, A4, A5, WAYBEL_0: 51;

       ex_sup_of (X,L) by YELLOW_0: 17;

      then ( sup X) = ( sup F) by A3, A4, A5, WAYBEL_0: 54;

      then

      consider d be Element of L such that

       A7: d in F and

       A8: x <= d by A1, A2;

      consider Y be finite Subset of X such that ex_sup_of (Y,L) and

       A9: d = ( "\/" (Y,L)) by A3, A7;

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

      take Y;

      thus thesis by A8, A9;

    end;

    theorem :: WAYBEL_3:19

    for L be complete LATTICE, x,y be Element of L st for X be Subset of L st y <= ( sup X) holds ex A be finite Subset of L st A c= X & x <= ( sup A) holds x << y

    proof

      let L be complete LATTICE, x,y be Element of L such that

       A1: for X be Subset of L st y <= ( sup X) holds ex A be finite Subset of L st A c= X & x <= ( sup A);

      let D be non empty directed Subset of L;

      assume y <= ( sup D);

      then

      consider A be finite Subset of L such that

       A2: A c= D and

       A3: x <= ( sup A) by A1;

      reconsider B = A as finite Subset of D by A2;

      consider a be Element of L such that

       A4: a in D and

       A5: a is_>=_than B by WAYBEL_0: 1;

      take a;

      a >= ( sup A) by A5, YELLOW_0: 32;

      hence thesis by A3, A4, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL_3:20

    for L be non empty reflexive transitive RelStr holds for x,y be Element of L st x << y holds for I be Ideal of L st y <= ( sup I) holds x in I

    proof

      let L be non empty reflexive transitive RelStr;

      let x,y be Element of L;

      assume

       A1: x << y;

      let I be Ideal of L;

      assume y <= ( sup I);

      then ex d be Element of L st d in I & x <= d by A1;

      hence thesis by WAYBEL_0:def 19;

    end;

    theorem :: WAYBEL_3:21

    

     Th21: for L be up-complete non empty Poset, x,y be Element of L st for I be Ideal of L st y <= ( sup I) holds x in I holds x << y

    proof

      let L be up-complete non empty Poset;

      let x,y be Element of L;

      assume

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

      let D be non empty directed Subset of L;

      assume

       A2: y <= ( sup D);

       ex_sup_of (D,L) by WAYBEL_0: 75;

      then ( sup D) = ( sup ( downarrow D)) by WAYBEL_0: 33;

      then x in ( downarrow D) by A1, A2;

      then ex d be Element of L st x <= d & d in D by WAYBEL_0:def 15;

      hence thesis;

    end;

    theorem :: WAYBEL_3:22

    for L be lower-bounded LATTICE st L is meet-continuous holds for x,y be Element of L holds x << y iff for I be Ideal of L st y = ( sup I) holds x in I

    proof

      let L be lower-bounded LATTICE;

      assume

       A1: L is up-complete satisfying_MC;

      let x,y be Element of L;

      hereby

        assume

         A2: x << y;

        let I be Ideal of L;

        assume y = ( sup I);

        then ex d be Element of L st d in I & x <= d by A2;

        hence x in I by WAYBEL_0:def 19;

      end;

      assume

       A3: for I be Ideal of L st y = ( sup I) holds x in I;

      now

        let I be Ideal of L;

        

         A4: ex_sup_of (( finsups ( {y} "/\" I)),L) by A1, WAYBEL_0: 75;

        assume y <= ( sup I);

        then (y "/\" ( sup I)) = y by YELLOW_0: 25;

        

        then y = ( sup ( {y} "/\" I)) by A1

        .= ( sup ( finsups ( {y} "/\" I))) by A1, WAYBEL_0: 55

        .= ( sup ( downarrow ( finsups ( {y} "/\" I)))) by A4, WAYBEL_0: 33;

        then x in ( downarrow ( finsups ( {y} "/\" I))) by A3;

        then

        consider z be Element of L such that

         A5: x <= z and

         A6: z in ( finsups ( {y} "/\" I)) by WAYBEL_0:def 15;

        consider Y be finite Subset of ( {y} "/\" I) such that

         A7: z = ( "\/" (Y,L)) and ex_sup_of (Y,L) by A6;

        set i = the Element of I;

        reconsider i as Element of L;

        

         A8: ex_sup_of ( {i},L) by YELLOW_0: 38;

        

         A9: ( sup {i}) = i by YELLOW_0: 39;

         ex_sup_of ( {} ,L) by A1, YELLOW_0: 17;

        then ( "\/" ( {} ,L)) <= ( sup {i}) by A8, XBOOLE_1: 2, YELLOW_0: 34;

        then

         A10: ( "\/" ( {} ,L)) in I by A9, WAYBEL_0:def 19;

        Y c= I

        proof

          let a be object;

          assume a in Y;

          then a in ( {y} "/\" I);

          then a in { (y "/\" j) where j be Element of L : j in I } by YELLOW_4: 42;

          then

          consider j be Element of L such that

           A11: a = (y "/\" j) and

           A12: j in I;

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

          hence thesis by A11, A12, WAYBEL_0:def 19;

        end;

        then z in I by A7, A10, WAYBEL_0: 42;

        hence x in I by A5, WAYBEL_0:def 19;

      end;

      hence thesis by A1, Th21;

    end;

    theorem :: WAYBEL_3:23

    for L be complete LATTICE holds (for x be Element of L holds x is compact) iff for X be non empty Subset of L holds ex x be Element of L st x in X & for y be Element of L st y in X holds not x < y

    proof

      let L be complete LATTICE;

      hereby

        assume

         A1: for x be Element of L holds x is compact;

        given Y be non empty Subset of L such that

         A2: for x be Element of L st x in Y holds ex y be Element of L st y in Y & x < y;

        defpred P[ object, object] means [$1, $2] in the InternalRel of L & $1 <> $2;

         A3:

        now

          let x be object;

          assume

           A4: x in Y;

          then

          reconsider y = x as Element of L;

          consider z be Element of L such that

           A5: z in Y and

           A6: y < z by A2, A4;

          reconsider u = z as object;

          take u;

          y <= z by A6;

          hence u in Y & P[x, u] by A5, A6;

        end;

        consider f be Function such that

         A7: ( dom f) = Y & ( rng f) c= Y & for x be object st x in Y holds P[x, (f . x)] from FUNCT_1:sch 6( A3);

        set x = the Element of Y;

        set x1 = x;

        set Z = the set of all (( iter (f,n)) . x) where n be Element of NAT ;

        (f . x) in ( rng f) by A7, FUNCT_1:def 3;

        then (f . x) in Y by A7;

        then

        reconsider x, x9 = (f . x1) as Element of L;

        

         A8: [x, (f . x)] in the InternalRel of L by A7;

        

         A9: x <> (f . x) by A7;

        

         A10: x9 = (( iter (f,1)) . x) by FUNCT_7: 70;

        

         A11: x <= x9 by A8;

        

         A12: x9 in Z by A10;

        

         A13: x < x9 by A9, A11;

        

         A14: Z c= Y

        proof

          let a be object;

          assume a in Z;

          then

          consider n be Element of NAT such that

           A15: a = (( iter (f,n)) . x);

          ( dom ( iter (f,n))) = Y by A7, FUNCT_7: 74;

          then

           A16: a in ( rng ( iter (f,n))) by A15, FUNCT_1:def 3;

          ( rng ( iter (f,n))) c= Y by A7, FUNCT_7: 74;

          hence thesis by A16;

        end;

        then

        reconsider Z as Subset of L by XBOOLE_1: 1;

         A17:

        now

          let i be Element of NAT ;

          defpred P[ Nat] means ex z,y be Element of L st z = (( iter (f,i)) . x) & y = (( iter (f,(i + $1))) . x) & z <= y;

          (( iter (f,i)) . x) in Z;

          then

           A18: P[ 0 ];

          

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

          proof

            let k be Nat;

            given z,y be Element of L such that

             A20: z = (( iter (f,i)) . x) and

             A21: y = (( iter (f,(i + k))) . x) and

             A22: z <= y;

            take z;

            

             A23: ( rng ( iter (f,(i + k)))) c= Y by A7, FUNCT_7: 74;

            

             A24: ( dom ( iter (f,(i + k)))) = Y by A7, FUNCT_7: 74;

            then

             A25: y in ( rng ( iter (f,(i + k)))) by A21, FUNCT_1:def 3;

            then (f . y) in ( rng f) by A7, A23, FUNCT_1:def 3;

            then (f . y) in Y by A7;

            then

            reconsider yy = (f . y) as Element of L;

            take yy;

            thus z = (( iter (f,i)) . x) by A20;

            ( iter (f,((k + i) + 1))) = (f * ( iter (f,(k + i)))) by FUNCT_7: 71;

            hence yy = (( iter (f,(i + (k + 1)))) . x) by A21, A24, FUNCT_1: 13;

             [y, yy] in the InternalRel of L by A7, A23, A25;

            then y <= yy;

            hence thesis by A22, ORDERS_2: 3;

          end;

          

           A26: for k be Nat holds P[k] from NAT_1:sch 2( A18, A19);

          let k be Element of NAT ;

          assume i <= k;

          then

          consider n be Nat such that

           A27: k = (i + n) by NAT_1: 10;

          reconsider n as Element of NAT by ORDINAL1:def 12;

          

           A28: ex z,y be Element of L st z = (( iter (f,i)) . x) & y = (( iter (f,(i + n))) . x) & z <= y by A26;

          let z,y be Element of L;

          assume that

           A29: z = (( iter (f,i)) . x) and

           A30: y = (( iter (f,k)) . x);

          thus z <= y by A27, A28, A29, A30;

        end;

         A31:

        now

          let z,y be Element of L;

          assume z in Z;

          then

          consider k1 be Element of NAT such that

           A32: z = (( iter (f,k1)) . x);

          assume y in Z;

          then

          consider k2 be Element of NAT such that

           A33: y = (( iter (f,k2)) . x);

          k1 <= k2 or k2 <= k1;

          hence z <= y or z >= y by A17, A32, A33;

        end;

        ( sup Z) is compact by A1;

        then ( sup Z) << ( sup Z);

        then

        consider A be finite Subset of L such that

         A34: A c= Z and

         A35: ( sup Z) <= ( sup A) by Th18;

         A36:

        now

          assume A = {} ;

          then x is_>=_than A;

          then ( sup A) <= x by YELLOW_0: 32;

          then

           A37: ( sup A) < x9 by A13, ORDERS_2: 7;

          

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

          

           A39: ( sup Z) < x9 by A35, A37, ORDERS_2: 7;

          x9 <= ( sup Z) by A12, A38;

          hence contradiction by A39, ORDERS_2: 6;

        end;

        

         A40: A is finite;

        defpred P[ set] means $1 <> {} implies ( "\/" ($1,L)) in $1;

        

         A41: P[ {} ];

         A42:

        now

          let x,B be set;

          assume that

           A43: x in A and

           A44: B c= A;

          reconsider x9 = x as Element of L by A43;

          assume

           A45: P[B];

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

          proof

            assume (B \/ {x}) <> {} ;

            

             A46: ex_sup_of (B,L) by YELLOW_0: 17;

            

             A47: ex_sup_of ( {x},L) by YELLOW_0: 17;

             ex_sup_of ((B \/ {x}),L) by YELLOW_0: 17;

            then

             A48: ( "\/" ((B \/ {x}),L)) = (( "\/" (B,L)) "\/" ( "\/" ( {x},L))) by A46, A47, YELLOW_0: 36;

            

             A49: ( sup {x9}) = x by YELLOW_0: 39;

            per cases ;

              suppose B = {} ;

              hence thesis by A49, TARSKI:def 1;

            end;

              suppose B <> {} ;

              then ( "\/" (B,L)) in A by A44, A45;

              then x9 <= ( "\/" (B,L)) or x9 >= ( "\/" (B,L)) by A31, A34, A43;

              then (( "\/" (B,L)) "\/" x9) = ( "\/" (B,L)) or (( "\/" (B,L)) "\/" x9) = (x9 "\/" ( "\/" (B,L))) & (x9 "\/" ( "\/" (B,L))) = x9 by YELLOW_0: 24;

              then ( "\/" ((B \/ {x}),L)) in B or ( "\/" ((B \/ {x}),L)) in {x} by A45, A48, A49, TARSKI:def 1;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

        end;

         P[A] from FINSET_1:sch 2( A40, A41, A42);

        then

         A50: ( sup A) in Z by A34, A36;

        then

        consider n be Element of NAT such that

         A51: ( sup A) = (( iter (f,n)) . x);

        

         A52: [( sup A), (f . ( sup A))] in the InternalRel of L by A7, A14, A50;

        

         A53: ( sup A) <> (f . ( sup A)) by A7, A14, A50;

        reconsider xSn = (f . ( sup A)) as Element of L by A52, ZFMISC_1: 87;

        

         A54: ( iter (f,(n + 1))) = (f * ( iter (f,n))) by FUNCT_7: 71;

        

         A55: ( dom ( iter (f,n))) = Y by A7, FUNCT_7: 74;

        

         A56: ( sup A) <= xSn by A52;

        

         A57: (f . ( sup A)) = (( iter (f,(n + 1))) . x) by A51, A54, A55, FUNCT_1: 13;

        

         A58: ( sup A) < xSn by A53, A56;

        

         A59: xSn in Z by A57;

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

        then

         A60: xSn <= ( sup Z) by A59;

        ( sup Z) < xSn by A35, A58, ORDERS_2: 7;

        hence contradiction by A60, ORDERS_2: 6;

      end;

      assume

       A61: for X be non empty Subset of L holds ex x be Element of L st x in X & for y be Element of L st y in X holds not x < y;

      let x be Element of L;

      let D be directed non empty Subset of L;

      consider y be Element of L such that

       A62: y in D and

       A63: for z be Element of L st z in D holds not y < z by A61;

      D is_<=_than y

      proof

        let a be Element of L;

        assume a in D;

        then

        consider b be Element of L such that

         A64: b in D and

         A65: a <= b and

         A66: y <= b by A62, WAYBEL_0:def 1;

         not y < b by A63, A64;

        hence thesis by A65, A66;

      end;

      then

       A67: ( sup D) <= y by YELLOW_0: 32;

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

      then y <= ( sup D) by A62;

      then ( sup D) = y by A67, ORDERS_2: 2;

      hence thesis by A62;

    end;

    begin

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL_3:def5

      attr L is satisfying_axiom_of_approximation means

      : Def5: for x be Element of L holds x = ( sup ( waybelow x));

    end

    registration

      cluster -> satisfying_axiom_of_approximation for 1 -element reflexive RelStr;

      coherence by ZFMISC_1:def 10;

    end

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL_3:def6

      attr L is continuous means

      : Def6: (for x be Element of L holds ( waybelow x) is non empty directed) & L is up-complete satisfying_axiom_of_approximation;

    end

    registration

      cluster continuous -> up-complete satisfying_axiom_of_approximation for non empty reflexive RelStr;

      coherence ;

      cluster up-complete satisfying_axiom_of_approximation -> continuous for lower-bounded sup-Semilattice;

      coherence ;

    end

    registration

      cluster continuous complete strict for LATTICE;

      existence

      proof

        set x = the set, R = the Order of {x};

         RelStr (# {x}, R #) is 1 -element RelStr;

        hence thesis;

      end;

    end

    registration

      let L be continuous non empty reflexive RelStr;

      let x be Element of L;

      cluster ( waybelow x) -> non empty directed;

      coherence by Def6;

    end

    theorem :: WAYBEL_3:24

    for L be up-complete Semilattice st for x be Element of L holds ( waybelow x) is non empty directed holds L is satisfying_axiom_of_approximation iff for x,y be Element of L st not x <= y holds ex u be Element of L st u << x & not u <= y

    proof

      let L be up-complete Semilattice such that

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

      hereby

        assume

         A2: L is satisfying_axiom_of_approximation;

        let x,y be Element of L;

        assume

         A3: not x <= y;

        

         A4: ( waybelow x) is non empty directed by A1;

        

         A5: x = ( sup ( waybelow x)) by A2;

         ex_sup_of (( waybelow x),L) by A4, WAYBEL_0: 75;

        then y is_>=_than ( waybelow x) implies y >= x by A5, YELLOW_0:def 9;

        then

        consider u be Element of L such that

         A6: u in ( waybelow x) and

         A7: not u <= y by A3;

        take u;

        thus u << x & not u <= y by A6, A7, Th7;

      end;

      assume

       A8: for x,y be Element of L st not x <= y holds ex u be Element of L st u << x & not u <= y;

      let x be Element of L;

      ( waybelow x) is non empty directed by A1;

      then

       A9: ex_sup_of (( waybelow x),L) by WAYBEL_0: 75;

      

       A10: x is_>=_than ( waybelow x) by Th9;

      now

        let y be Element of L;

        assume that

         A11: y is_>=_than ( waybelow x) and

         A12: not x <= y;

        consider u be Element of L such that

         A13: u << x and

         A14: not u <= y by A8, A12;

        u in ( waybelow x) by A13;

        hence contradiction by A11, A14;

      end;

      hence thesis by A9, A10, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL_3:25

    for L be continuous LATTICE, x,y be Element of L holds x <= y iff ( waybelow x) c= ( waybelow y)

    proof

      let L be continuous LATTICE, x,y be Element of L;

      thus x <= y implies ( waybelow x) c= ( waybelow y) by Th12;

      assume

       A1: ( waybelow x) c= ( waybelow y);

      

       A2: ex_sup_of (( waybelow x),L) by WAYBEL_0: 75;

       ex_sup_of (( waybelow y),L) by WAYBEL_0: 75;

      then ( sup ( waybelow x)) <= ( sup ( waybelow y)) by A1, A2, YELLOW_0: 34;

      then x <= ( sup ( waybelow y)) by Def5;

      hence thesis by Def5;

    end;

    registration

      cluster complete -> satisfying_axiom_of_approximation for non empty Chain;

      coherence

      proof

        let L be non empty Chain;

        assume L is complete;

        then

        reconsider S = L as complete non empty Chain;

        S is satisfying_axiom_of_approximation

        proof

          let x be Element of S;

          

           A1: ex_sup_of (( waybelow x),S) by YELLOW_0: 17;

          

           A2: x is_>=_than ( waybelow x) by Th9;

          now

            let y be Element of S;

            assume that

             A3: y is_>=_than ( waybelow x) and

             A4: not x <= y;

            x >= y by A4, WAYBEL_0:def 29;

            then x > y by A4;

            then x >> y by Th13;

            then y in ( waybelow x);

            then for z be Element of S st z is_>=_than ( waybelow x) holds z >= y;

            then

             A5: ( sup ( waybelow x)) = y by A1, A3, YELLOW_0:def 9;

            x << x

            proof

              let D be non empty directed Subset of S;

              assume

               A6: x <= ( sup D);

              assume

               A7: for d be Element of S st d in D holds not x <= d;

              

               A8: D c= ( waybelow x)

              proof

                let a be object;

                assume

                 A9: a in D;

                then

                reconsider a as Element of S;

                

                 A10: not x <= a by A7, A9;

                then a <= x by WAYBEL_0:def 29;

                then a < x by A10;

                then a << x by Th13;

                hence thesis;

              end;

               ex_sup_of (D,S) by YELLOW_0: 17;

              then ( sup D) <= ( sup ( waybelow x)) by A1, A8, YELLOW_0: 34;

              hence contradiction by A4, A5, A6, ORDERS_2: 3;

            end;

            then x in ( waybelow x);

            hence contradiction by A3, A4;

          end;

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

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_3:26

    for L be complete LATTICE st for x be Element of L holds x is compact holds L is satisfying_axiom_of_approximation

    proof

      let L be complete LATTICE such that

       A1: for x be Element of L holds x is compact;

      let x be Element of L;

      x is compact by A1;

      then x << x;

      then

       A2: x in ( waybelow x);

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

      then

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

      

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

      

       A5: ex_sup_of (( downarrow x),L) by WAYBEL_0: 34;

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

      then x >= ( sup ( waybelow x)) by A4, A5, Th11, YELLOW_0: 34;

      hence thesis by A3, ORDERS_2: 2;

    end;

    begin

    definition

      let f be Relation;

      :: WAYBEL_3:def7

      attr f is non-Empty means

      : Def7: for S be 1-sorted st S in ( rng f) holds S is non empty;

      :: WAYBEL_3:def8

      attr f is reflexive-yielding means

      : Def8: for S be RelStr st S in ( rng f) holds S is reflexive;

    end

    registration

      let I be set;

      cluster RelStr-yielding non-Empty reflexive-yielding for ManySortedSet of I;

      existence

      proof

        set R = the reflexive non empty RelStr;

        set J = (I --> R);

        

         A1: ( rng J) c= {R} by FUNCOP_1: 13;

        reconsider J as ManySortedSet of I;

        take J;

        thus J is RelStr-yielding;

        thus J is non-Empty by A1, TARSKI:def 1;

        let S be RelStr;

        assume S in ( rng J);

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    registration

      let I be set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      cluster ( product J) -> non empty;

      coherence

      proof

        

         A1: the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

        now

          assume {} in ( rng ( Carrier J));

          then

          consider i be object such that

           A2: i in ( dom ( Carrier J)) and

           A3: {} = (( Carrier J) . i) by FUNCT_1:def 3;

          

           A4: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

          

           A5: ( dom J) = I by PARTFUN1:def 2;

          consider R be 1-sorted such that

           A6: R = (J . i) and

           A7: {} = the carrier of R by A2, A3, A4, PRALG_1:def 15;

          R in ( rng J) by A2, A4, A5, A6, FUNCT_1:def 3;

          then

          reconsider R as non empty RelStr by Def7, YELLOW_1:def 3;

          the carrier of R = {} by A7;

          hence contradiction;

        end;

        then the carrier of ( product J) <> {} by A1, CARD_3: 26;

        hence thesis;

      end;

    end

    definition

      let I be non empty set;

      let J be RelStr-yielding ManySortedSet of I;

      let i be Element of I;

      :: original: .

      redefine

      func J . i -> RelStr ;

      coherence

      proof

        ( dom J) = I by PARTFUN1:def 2;

        then (J . i) in ( rng J) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    registration

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      let i be Element of I;

      cluster (J . i) -> non empty;

      coherence

      proof

        ( dom J) = I by PARTFUN1:def 2;

        then (J . i) in ( rng J) by FUNCT_1:def 3;

        hence thesis by Def7;

      end;

    end

    registration

      let I be set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      cluster ( product J) -> constituted-Functions;

      coherence

      proof

        the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

        hence thesis by MONOID_0: 80;

      end;

    end

    definition

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      let x be Element of ( product J);

      let i be Element of I;

      :: original: .

      redefine

      func x . i -> Element of (J . i) ;

      coherence

      proof

        

         A1: ex R be 1-sorted st R = (J . i) & (( Carrier J) . i) = the carrier of R by PRALG_1:def 15;

        

         A2: the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

        ( dom ( Carrier J)) = I by PARTFUN1:def 2;

        hence thesis by A1, A2, CARD_3: 9;

      end;

    end

    definition

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      let i be Element of I;

      let X be Subset of ( product J);

      :: original: pi

      redefine

      func pi (X,i) -> Subset of (J . i) ;

      coherence

      proof

        set Y = the carrier of ( product J);

        

         A1: Y = ( product ( Carrier J)) by YELLOW_1:def 4;

        

         A2: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

        (X \/ Y) = Y by XBOOLE_1: 12;

        then ( pi (Y,i)) = (( pi (X,i)) \/ ( pi (Y,i))) by CARD_3: 16;

        then

         A3: ( pi (X,i)) c= ( pi (Y,i)) by XBOOLE_1: 7;

        ex R be 1-sorted st R = (J . i) & (( Carrier J) . i) = the carrier of R by PRALG_1:def 15;

        hence thesis by A1, A2, A3, CARD_3: 12;

      end;

    end

    theorem :: WAYBEL_3:27

    

     Th27: for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I holds for x be Function holds x is Element of ( product J) iff ( dom x) = I & for i be Element of I holds (x . i) is Element of (J . i)

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      let x be Function;

      

       A1: the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

      

       A2: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

      hereby

        assume

         A3: x is Element of ( product J);

        hence ( dom x) = I by A1, A2, CARD_3: 9;

        let i be Element of I;

        reconsider y = x as Element of ( product J) by A3;

        (y . i) is Element of (J . i);

        hence (x . i) is Element of (J . i);

      end;

      assume that

       A4: ( dom x) = I and

       A5: for i be Element of I holds (x . i) is Element of (J . i);

      now

        let i be object;

        assume i in ( dom ( Carrier J));

        then

        reconsider j = i as Element of I by PARTFUN1:def 2;

        

         A6: (x . j) is Element of (J . j) by A5;

        ex R be 1-sorted st R = (J . j) & (( Carrier J) . j) = the carrier of R by PRALG_1:def 15;

        hence (x . i) in (( Carrier J) . i) by A6;

      end;

      hence thesis by A1, A2, A4, CARD_3: 9;

    end;

    theorem :: WAYBEL_3:28

    

     Th28: for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I holds for x,y be Element of ( product J) holds x <= y iff for i be Element of I holds (x . i) <= (y . i)

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      set L = ( product J);

      let x,y be Element of L;

      

       A1: the carrier of L = ( product ( Carrier J)) by YELLOW_1:def 4;

      hereby

        assume

         A2: x <= y;

        let i be Element of I;

        ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A1, A2, YELLOW_1:def 4;

        then ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (x . i) & yi = (y . i) & xi <= yi;

        hence (x . i) <= (y . i);

      end;

      assume

       A3: for i be Element of I holds (x . i) <= (y . i);

      ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi

      proof

        take f = x, g = y;

        thus f = x & g = y;

        let i be object;

        assume i in I;

        then

        reconsider j = i as Element of I;

        take (J . j), (x . j), (y . j);

        thus thesis by A3;

      end;

      hence thesis by A1, YELLOW_1:def 4;

    end;

    registration

      let I be non empty set;

      let J be RelStr-yielding reflexive-yielding ManySortedSet of I;

      let i be Element of I;

      cluster (J . i) -> reflexive;

      coherence

      proof

        ( dom J) = I by PARTFUN1:def 2;

        then (J . i) in ( rng J) by FUNCT_1:def 3;

        hence thesis by Def8;

      end;

    end

    registration

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      cluster ( product J) -> reflexive;

      coherence

      proof

        thus ( product J) is reflexive

        proof

          let x be Element of ( product J);

          for i be Element of I holds (x . i) <= (x . i);

          hence thesis by Th28;

        end;

      end;

    end

    theorem :: WAYBEL_3:29

    

     Th29: for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is transitive holds ( product J) is transitive

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is transitive;

      let x,y,z be Element of ( product J) such that

       A2: x <= y and

       A3: y <= z;

      now

        let i be Element of I;

        

         A4: (x . i) <= (y . i) by A2, Th28;

        

         A5: (y . i) <= (z . i) by A3, Th28;

        (J . i) is transitive by A1;

        hence (x . i) <= (z . i) by A4, A5;

      end;

      hence thesis by Th28;

    end;

    theorem :: WAYBEL_3:30

    

     Th30: for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is antisymmetric holds ( product J) is antisymmetric

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is antisymmetric;

      let x,y be Element of ( product J) such that

       A2: x <= y and

       A3: y <= x;

      

       A4: ( dom x) = I by Th27;

      

       A5: ( dom y) = I by Th27;

      now

        let j be object;

        assume j in I;

        then

        reconsider i = j as Element of I;

        

         A6: (x . i) <= (y . i) by A2, Th28;

        

         A7: (y . i) <= (x . i) by A3, Th28;

        (J . i) is antisymmetric by A1;

        hence (x . j) = (y . j) by A6, A7;

      end;

      hence thesis by A4, A5, FUNCT_1: 2;

    end;

    theorem :: WAYBEL_3:31

    

     Th31: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is complete LATTICE holds ( product J) is complete LATTICE

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J . i) is complete LATTICE;

      then

       A2: for i be Element of I holds (J . i) is transitive;

      for i be Element of I holds (J . i) is antisymmetric by A1;

      then

      reconsider L = ( product J) as non empty Poset by A2, Th29, Th30;

      now

        let X be Subset of ( product J);

        deffunc F( Element of I) = ( sup ( pi (X,$1)));

        consider f be ManySortedSet of I such that

         A3: for i be Element of I holds (f . i) = F(i) from PBOOLE:sch 5;

        

         A4: ( dom f) = I by PARTFUN1:def 2;

        now

          let i be Element of I;

          (f . i) = ( sup ( pi (X,i))) by A3;

          hence (f . i) is Element of (J . i);

        end;

        then

        reconsider f as Element of ( product J) by A4, Th27;

        

         A5: f is_>=_than X

        proof

          let x be Element of ( product J) such that

           A6: x in X;

          now

            let i be Element of I;

            

             A7: (x . i) in ( pi (X,i)) by A6, CARD_3:def 6;

            

             A8: (J . i) is complete LATTICE by A1;

            (f . i) = ( sup ( pi (X,i))) by A3;

            hence (x . i) <= (f . i) by A7, A8, YELLOW_2: 22;

          end;

          hence thesis by Th28;

        end;

        now

          let g be Element of ( product J);

          assume

           A9: X is_<=_than g;

          now

            thus L = L;

            let i be Element of I;

            

             A10: (f . i) = ( sup ( pi (X,i))) by A3;

            

             A11: (J . i) is complete LATTICE by A1;

            (g . i) is_>=_than ( pi (X,i))

            proof

              let a be Element of (J . i);

              assume a in ( pi (X,i));

              then

              consider h be Function such that

               A12: h in X and

               A13: a = (h . i) by CARD_3:def 6;

              reconsider h as Element of ( product J) by A12;

              h <= g by A9, A12;

              hence a <= (g . i) by A13, Th28;

            end;

            hence (f . i) <= (g . i) by A10, A11, YELLOW_0: 32;

          end;

          hence f <= g by Th28;

        end;

        then ex_sup_of (X,L) by A5, YELLOW_0: 15;

        hence ex_sup_of (X,( product J));

      end;

      then L is complete non empty Poset by YELLOW_0: 53;

      hence thesis;

    end;

    theorem :: WAYBEL_3:32

    

     Th32: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is complete LATTICE holds for X be Subset of ( product J), i be Element of I holds (( sup X) . i) = ( sup ( pi (X,i)))

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J . i) is complete LATTICE;

      then

      reconsider L = ( product J) as complete LATTICE by Th31;

      

       A2: L is complete;

      let X be Subset of ( product J), i be Element of I;

      

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

      

       A4: (( sup X) . i) is_>=_than ( pi (X,i))

      proof

        let a be Element of (J . i);

        assume a in ( pi (X,i));

        then

        consider f be Function such that

         A5: f in X and

         A6: a = (f . i) by CARD_3:def 6;

        reconsider f as Element of ( product J) by A5;

        ( sup X) >= f by A3, A5;

        hence thesis by A6, Th28;

      end;

      

       A7: (J . i) is complete LATTICE by A1;

      now

        let a be Element of (J . i);

        assume

         A8: a is_>=_than ( pi (X,i));

        set f = (( sup X) +* (i,a));

        

         A9: ( dom f) = ( dom ( sup X)) by FUNCT_7: 30;

        

         A10: ( dom ( sup X)) = I by Th27;

        now

          let j be Element of I;

          j = i or j <> i;

          then (f . j) = (( sup X) . j) or (f . j) = a & j = i by A10, FUNCT_7: 31, FUNCT_7: 32;

          hence (f . j) is Element of (J . j);

        end;

        then

        reconsider f as Element of ( product J) by A9, Th27;

        f is_>=_than X

        proof

          let g be Element of ( product J);

          assume

           A11: g in X;

          then

           A12: g <= ( sup X) by A2, YELLOW_2: 22;

          

           A13: (g . i) in ( pi (X,i)) by A11, CARD_3:def 6;

          now

            let j be Element of I;

            j = i or j <> i;

            then (f . j) = (( sup X) . j) or (f . j) = a & j = i by A10, FUNCT_7: 31, FUNCT_7: 32;

            hence (f . j) >= (g . j) by A8, A12, A13, Th28;

          end;

          hence thesis by Th28;

        end;

        then

         A14: f >= ( sup X) by A2, YELLOW_0: 32;

        (f . i) = a by A10, FUNCT_7: 31;

        hence (( sup X) . i) <= a by A14, Th28;

      end;

      hence thesis by A4, A7, YELLOW_0: 32;

    end;

    theorem :: WAYBEL_3:33

    for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is complete LATTICE holds for x,y be Element of ( product J) holds x << y iff (for i be Element of I holds (x . i) << (y . i)) & ex K be finite Subset of I st for i be Element of I st not i in K holds (x . i) = ( Bottom (J . i))

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      set L = ( product J);

      assume

       A1: for i be Element of I holds (J . i) is complete LATTICE;

      then

      reconsider L9 = L as complete LATTICE by Th31;

      let x,y be Element of L;

      hereby

        assume

         A2: x << y;

        hereby

          let i be Element of I;

          thus (x . i) << (y . i)

          proof

            let Di be non empty directed Subset of (J . i) such that

             A3: (y . i) <= ( sup Di);

            

             A4: ( dom y) = I by Th27;

            set D = { (y +* (i,z)) where z be Element of (J . i) : z in Di };

            D c= the carrier of L

            proof

              let a be object;

              assume a in D;

              then

              consider z be Element of (J . i) such that

               A5: a = (y +* (i,z)) and z in Di;

              

               A6: ( dom (y +* (i,z))) = I by A4, FUNCT_7: 30;

              now

                let j be Element of I;

                i = j or i <> j;

                then ((y +* (i,z)) . j) = z & i = j or ((y +* (i,z)) . j) = (y . j) by A4, FUNCT_7: 31, FUNCT_7: 32;

                hence ((y +* (i,z)) . j) is Element of (J . j);

              end;

              then a is Element of L by A5, A6, Th27;

              hence thesis;

            end;

            then

            reconsider D as Subset of L;

            set di = the Element of Di;

            reconsider di as Element of (J . i);

            

             A7: (y +* (i,di)) in D;

            

             A8: ( dom y) = I by Th27;

            reconsider D as non empty Subset of L by A7;

            D is directed

            proof

              let z1,z2 be Element of L;

              assume z1 in D;

              then

              consider a1 be Element of (J . i) such that

               A9: z1 = (y +* (i,a1)) and

               A10: a1 in Di;

              assume z2 in D;

              then

              consider a2 be Element of (J . i) such that

               A11: z2 = (y +* (i,a2)) and

               A12: a2 in Di;

              consider a be Element of (J . i) such that

               A13: a in Di and

               A14: a >= a1 and

               A15: a >= a2 by A10, A12, WAYBEL_0:def 1;

              (y +* (i,a)) in D by A13;

              then

              reconsider z = (y +* (i,a)) as Element of L;

              take z;

              thus z in D by A13;

              

               A16: ( dom y) = I by Th27;

              now

                let j be Element of I;

                i = j or i <> j;

                then (z . j) = a & (z1 . j) = a1 & i = j or (z . j) = (y . j) & (z1 . j) = (y . j) by A9, A16, FUNCT_7: 31, FUNCT_7: 32;

                hence (z . j) >= (z1 . j) by A14, YELLOW_0:def 1;

              end;

              hence z >= z1 by Th28;

              now

                let j be Element of I;

                i = j or i <> j;

                then (z . j) = a & (z2 . j) = a2 & i = j or (z . j) = (y . j) & (z2 . j) = (y . j) by A11, A16, FUNCT_7: 31, FUNCT_7: 32;

                hence (z . j) >= (z2 . j) by A15, YELLOW_0:def 1;

              end;

              hence thesis by Th28;

            end;

            then

            reconsider D as non empty directed Subset of L;

            now

              let j be Element of I;

              

               A17: (J . i) is complete LATTICE by A1;

              

               A18: (J . j) is complete LATTICE by A1;

              

               A19: ex_sup_of (Di,(J . i)) by A17, YELLOW_0: 17;

              

               A20: ex_sup_of (( pi (D,i)),(J . i)) by A17, YELLOW_0: 17;

              Di c= ( pi (D,i))

              proof

                let a be object;

                assume

                 A21: a in Di;

                then

                reconsider a as Element of (J . i);

                (y +* (i,a)) in D by A21;

                then ((y +* (i,a)) . i) in ( pi (D,i)) by CARD_3:def 6;

                hence thesis by A8, FUNCT_7: 31;

              end;

              then

               A22: ( sup Di) <= ( sup ( pi (D,i))) by A19, A20, YELLOW_0: 34;

              

               A23: (( sup D) . j) = ( sup ( pi (D,j))) by A1, Th32;

              now

                assume j <> i;

                then ((y +* (i,di)) . j) = (y . j) by FUNCT_7: 32;

                hence (y . j) in ( pi (D,j)) by A7, CARD_3:def 6;

              end;

              hence (( sup D) . j) >= (y . j) by A3, A18, A22, A23, YELLOW_0:def 2, YELLOW_2: 22;

            end;

            then ( sup D) >= y by Th28;

            then

            consider d be Element of L such that

             A24: d in D and

             A25: d >= x by A2;

            consider z be Element of (J . i) such that

             A26: d = (y +* (i,z)) and

             A27: z in Di by A24;

            take z;

            (d . i) = z by A4, A26, FUNCT_7: 31;

            hence thesis by A25, A27, Th28;

          end;

        end;

        set K = { i where i be Element of I : (x . i) <> ( Bottom (J . i)) };

        K c= I

        proof

          let a be object;

          assume a in K;

          then ex i be Element of I st a = i & (x . i) <> ( Bottom (J . i));

          hence thesis;

        end;

        then

        reconsider K as Subset of I;

        deffunc F( Element of I) = ( Bottom (J . $1));

        consider f be ManySortedSet of I such that

         A28: for i be Element of I holds (f . i) = F(i) from PBOOLE:sch 5;

        

         A29: ( dom f) = I by PARTFUN1:def 2;

        now

          let i be Element of I;

          (f . i) = ( Bottom (J . i)) by A28;

          hence (f . i) is Element of (J . i);

        end;

        then

        reconsider f as Element of ( product J) by A29, Th27;

        set X = the set of all (f +* (y | a)) where a be finite Subset of I;

        X c= the carrier of L

        proof

          let a be object;

          assume a in X;

          then

          consider b be finite Subset of I such that

           A30: a = (f +* (y | b));

          ( dom y) = I by Th27;

          then

           A31: ( dom (y | b)) = b by RELAT_1: 62;

          

          then

           A32: I = (I \/ ( dom (y | b))) by XBOOLE_1: 12

          .= ( dom (f +* (y | b))) by A29, FUNCT_4:def 1;

          now

            let i be Element of I;

            ((f +* (y | b)) . i) = (f . i) or ((f +* (y | b)) . i) = ((y | b) . i) & ((y | b) . i) = (y . i) by A31, FUNCT_1: 47, FUNCT_4: 11, FUNCT_4: 13;

            hence ((f +* (y | b)) . i) is Element of (J . i);

          end;

          then a is Element of L by A30, A32, Th27;

          hence thesis;

        end;

        then

        reconsider X as Subset of L;

        (f +* (y | ( {} I))) in X;

        then

        reconsider X as non empty Subset of L;

        X is directed

        proof

          let z1,z2 be Element of L;

          assume z1 in X;

          then

          consider a1 be finite Subset of I such that

           A33: z1 = (f +* (y | a1));

          assume z2 in X;

          then

          consider a2 be finite Subset of I such that

           A34: z2 = (f +* (y | a2));

          reconsider a = (a1 \/ a2) as finite Subset of I;

          (f +* (y | a)) in X;

          then

          reconsider z = (f +* (y | a)) as Element of L;

          take z;

          thus z in X;

          

           A35: ( dom y) = I by Th27;

          then

           A36: ( dom (y | a)) = a by RELAT_1: 62;

          

           A37: ( dom (y | a1)) = a1 by A35, RELAT_1: 62;

          

           A38: ( dom (y | a2)) = a2 by A35, RELAT_1: 62;

          now

            let i be Element of I;

            (J . i) is complete LATTICE by A1;

            then

             A39: ( Bottom (J . i)) <= (y . i) by YELLOW_0: 44;

            

             A40: (f . i) = ( Bottom (J . i)) by A28;

            per cases by XBOOLE_0:def 3;

              suppose

               A41: not i in a1 & i in a;

              then

               A42: (z . i) = ((y | a) . i) by A36, FUNCT_4: 13;

              ((y | a) . i) = (y . i) by A36, A41, FUNCT_1: 47;

              hence (z . i) >= (z1 . i) by A33, A37, A39, A40, A41, A42, FUNCT_4: 11;

            end;

              suppose

               A43: not i in a & not i in a1;

              then

               A44: (z . i) = (f . i) by A36, FUNCT_4: 11;

              (z1 . i) = (f . i) by A33, A37, A43, FUNCT_4: 11;

              hence (z . i) >= (z1 . i) by A44, YELLOW_0:def 1;

            end;

              suppose

               A45: i in a1 & i in a;

              then

               A46: (z . i) = ((y | a) . i) by A36, FUNCT_4: 13;

              

               A47: ((y | a) . i) = (y . i) by A36, A45, FUNCT_1: 47;

              

               A48: (z1 . i) = ((y | a1) . i) by A33, A37, A45, FUNCT_4: 13;

              ((y | a1) . i) = (y . i) by A37, A45, FUNCT_1: 47;

              hence (z . i) >= (z1 . i) by A46, A47, A48, YELLOW_0:def 1;

            end;

          end;

          hence z >= z1 by Th28;

          now

            let i be Element of I;

            (J . i) is complete LATTICE by A1;

            then

             A49: ( Bottom (J . i)) <= (y . i) by YELLOW_0: 44;

            

             A50: (f . i) = ( Bottom (J . i)) by A28;

            per cases by XBOOLE_0:def 3;

              suppose

               A51: not i in a2 & i in a;

              then

               A52: (z . i) = ((y | a) . i) by A36, FUNCT_4: 13;

              ((y | a) . i) = (y . i) by A36, A51, FUNCT_1: 47;

              hence (z . i) >= (z2 . i) by A34, A38, A49, A50, A51, A52, FUNCT_4: 11;

            end;

              suppose

               A53: not i in a & not i in a2;

              then

               A54: (z . i) = (f . i) by A36, FUNCT_4: 11;

              (z2 . i) = (f . i) by A34, A38, A53, FUNCT_4: 11;

              hence (z . i) >= (z2 . i) by A54, YELLOW_0:def 1;

            end;

              suppose

               A55: i in a2 & i in a;

              then

               A56: (z . i) = ((y | a) . i) by A36, FUNCT_4: 13;

              

               A57: ((y | a) . i) = (y . i) by A36, A55, FUNCT_1: 47;

              

               A58: (z2 . i) = ((y | a2) . i) by A34, A38, A55, FUNCT_4: 13;

              ((y | a2) . i) = (y . i) by A38, A55, FUNCT_1: 47;

              hence (z . i) >= (z2 . i) by A56, A57, A58, YELLOW_0:def 1;

            end;

          end;

          hence thesis by Th28;

        end;

        then

        reconsider X as non empty directed Subset of L;

        now

          let i be Element of I;

          reconsider a = {i} as finite Subset of I;

          

           A59: (f +* (y | a)) in X;

          

           A60: L = L9;

          reconsider z = (f +* (y | a)) as Element of L by A59;

          

           A61: ( dom y) = I by Th27;

          

           A62: i in a by TARSKI:def 1;

          then

           A63: ((y | a) . i) = (y . i) by FUNCT_1: 49;

          

           A64: ( dom (y | a)) = a by A61, RELAT_1: 62;

          

           A65: z <= ( sup X) by A59, A60, YELLOW_2: 22;

          (z . i) = (y . i) by A62, A63, A64, FUNCT_4: 13;

          hence (( sup X) . i) >= (y . i) by A65, Th28;

        end;

        then y <= ( sup X) by Th28;

        then

        consider d be Element of L such that

         A66: d in X and

         A67: x <= d by A2;

        consider a be finite Subset of I such that

         A68: d = (f +* (y | a)) by A66;

        K c= a

        proof

          let j be object;

          assume j in K;

          then

          consider i be Element of I such that

           A69: j = i and

           A70: (x . i) <> ( Bottom (J . i));

          assume

           A71: not j in a;

          ( dom y) = I by Th27;

          then ( dom (y | a)) = a by RELAT_1: 62;

          

          then

           A72: (d . i) = (f . i) by A68, A69, A71, FUNCT_4: 11

          .= ( Bottom (J . i)) by A28;

          

           A73: (J . i) is complete LATTICE by A1;

          

           A74: (x . i) <= (d . i) by A67, Th28;

          (x . i) >= ( Bottom (J . i)) by A73, YELLOW_0: 44;

          hence contradiction by A70, A72, A73, A74, ORDERS_2: 2;

        end;

        then

        reconsider K as finite Subset of I;

        take K;

        thus for i be Element of I st not i in K & (x . i) <> ( Bottom (J . i)) holds contradiction;

      end;

      assume

       A75: for i be Element of I holds (x . i) << (y . i);

      given K be finite Subset of I such that

       A76: for i be Element of I st not i in K holds (x . i) = ( Bottom (J . i));

      let D be non empty directed Subset of L such that

       A77: y <= ( sup D);

      defpred P[ object, object] means ex i be Element of I, z be Element of L st $1 = i & $2 = z & (z . i) >= (x . i);

       A78:

      now

        let k be object;

        assume k in K;

        then

        reconsider i = k as Element of I;

        

         A79: ( pi (D,i)) is directed

        proof

          let a,b be Element of (J . i);

          assume a in ( pi (D,i));

          then

          consider f be Function such that

           A80: f in D and

           A81: a = (f . i) by CARD_3:def 6;

          assume b in ( pi (D,i));

          then

          consider g be Function such that

           A82: g in D and

           A83: b = (g . i) by CARD_3:def 6;

          reconsider f, g as Element of L by A80, A82;

          consider h be Element of L such that

           A84: h in D and

           A85: h >= f and

           A86: h >= g by A80, A82, WAYBEL_0:def 1;

          take (h . i);

          thus thesis by A81, A83, A84, A85, A86, Th28, CARD_3:def 6;

        end;

        set dd = the Element of D;

        reconsider dd as Element of L;

        

         A87: (dd . i) in ( pi (D,i)) by CARD_3:def 6;

        

         A88: (x . i) << (y . i) by A75;

        

         A89: (y . i) <= (( sup D) . i) by A77, Th28;

        (( sup D) . i) = ( sup ( pi (D,i))) by A1, Th32;

        then

        consider zi be Element of (J . i) such that

         A90: zi in ( pi (D,i)) and

         A91: zi >= (x . i) by A79, A87, A88, A89;

        consider a be Function such that

         A92: a in D and

         A93: zi = (a . i) by A90, CARD_3:def 6;

        reconsider a as object;

        take a;

        thus a in D by A92;

        thus P[k, a] by A91, A92, A93;

      end;

      consider F be Function such that

       A94: ( dom F) = K & ( rng F) c= D and

       A95: for k be object st k in K holds P[k, (F . k)] from FUNCT_1:sch 6( A78);

      reconsider Y = ( rng F) as finite Subset of D by A94, FINSET_1: 8;

      L = L9;

      then

      consider d be Element of L such that

       A96: d in D and

       A97: d is_>=_than Y by WAYBEL_0: 1;

      take d;

      thus d in D by A96;

      now

        let i be Element of I;

        

         A98: (J . i) is complete LATTICE by A1;

        per cases ;

          suppose

           A99: i in K;

          then

          consider j be Element of I, z be Element of L such that

           A100: i = j and

           A101: (F . i) = z and

           A102: (z . j) >= (x . j) by A95;

          z in Y by A94, A99, A101, FUNCT_1:def 3;

          then d >= z by A97;

          then (d . i) >= (z . i) by Th28;

          hence (d . i) >= (x . i) by A98, A100, A102, YELLOW_0:def 2;

        end;

          suppose not i in K;

          then (x . i) = ( Bottom (J . i)) by A76;

          hence (d . i) >= (x . i) by A98, YELLOW_0: 44;

        end;

      end;

      hence thesis by Th28;

    end;

    begin

    theorem :: WAYBEL_3:34

    

     Th34: for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st x is_way_below y holds for F be Subset-Family of T st F is open & y c= ( union F) holds ex G be finite Subset of F st x c= ( union G)

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      let x,y be Element of L such that

       A1: x << y;

      let F be Subset-Family of T;

      assume that

       A2: F is open and

       A3: y c= ( union F);

      reconsider A = F as Subset of L by A2, YELLOW_1: 25;

      ( sup A) = ( union F) by YELLOW_1: 22;

      then y <= ( sup A) by A3, YELLOW_1: 3;

      then

      consider B be finite Subset of L such that

       A4: B c= A and

       A5: x <= ( sup B) by A1, Th18;

      reconsider G = B as finite Subset of F by A4;

      take G;

      ( sup B) = ( union G) by YELLOW_1: 22;

      hence thesis by A5, YELLOW_1: 3;

    end;

    theorem :: WAYBEL_3:35

    

     Th35: for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st for F be Subset-Family of T st F is open & y c= ( union F) holds ex G be finite Subset of F st x c= ( union G) holds x is_way_below y

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      

       A1: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      let x,y be Element of L such that

       A2: for F be Subset-Family of T st F is open & y c= ( union F) holds ex G be finite Subset of F st x c= ( union G);

      now

        let I be Ideal of L;

        reconsider F = I as Subset-Family of T by A1, XBOOLE_1: 1;

        assume y <= ( sup I);

        then y c= ( sup I) by YELLOW_1: 3;

        then

         A3: y c= ( union F) by YELLOW_1: 22;

        F is open by YELLOW_1: 25;

        then

        consider G be finite Subset of F such that

         A4: x c= ( union G) by A2, A3;

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

        consider z be Element of L such that

         A5: z in I and

         A6: z is_>=_than G by WAYBEL_0: 1;

        

         A7: ( union G) = ( sup G) by YELLOW_1: 22;

        

         A8: z >= ( sup G) by A6, YELLOW_0: 32;

        

         A9: x <= ( sup G) by A4, A7, YELLOW_1: 3;

        ( sup G) in I by A5, A8, WAYBEL_0:def 19;

        hence x in I by A9, WAYBEL_0:def 19;

      end;

      hence thesis by Th21;

    end;

    theorem :: WAYBEL_3:36

    

     Th36: for T be non empty TopSpace holds for x be Element of ( InclPoset the topology of T) holds for X be Subset of T st x = X holds x is compact iff X is compact

    proof

      let T be non empty TopSpace;

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

       A1: x = X;

      hereby

        assume x is compact;

        then

         A2: x << x;

        thus X is compact

        proof

          let F be Subset-Family of T such that

           A3: X c= ( union F) and

           A4: F is open;

          consider G be finite Subset of F such that

           A5: x c= ( union G) by A1, A2, A3, A4, Th34;

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

          take G;

          thus G c= F & X c= ( union G) & G is finite by A1, A5;

        end;

      end;

      assume

       A6: for F be Subset-Family of T st F is Cover of X & F is open holds ex G be Subset-Family of T st G c= F & G is Cover of X & G is finite;

      now

        let F be Subset-Family of T;

        assume that

         A7: F is open and

         A8: x c= ( union F);

        F is Cover of X by A1, A8, SETFAM_1:def 11;

        then

        consider G be Subset-Family of T such that

         A9: G c= F and

         A10: G is Cover of X and

         A11: G is finite by A6, A7;

        x c= ( union G) by A1, A10, SETFAM_1:def 11;

        hence ex G be finite Subset of F st x c= ( union G) by A9, A11;

      end;

      hence x << x by Th35;

    end;

    theorem :: WAYBEL_3:37

    for T be non empty TopSpace holds for x be Element of ( InclPoset the topology of T) st x = the carrier of T holds x is compact iff T is compact

    proof

      let T be non empty TopSpace;

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

      assume

       A1: x = the carrier of T;

      T is compact iff ( [#] T) is compact;

      hence thesis by A1, Th36;

    end;

    definition

      let T be non empty TopSpace;

      :: WAYBEL_3:def9

      attr T is locally-compact means for x be Point of T, X be Subset of T st x in X & X is open holds ex Y be Subset of T st x in ( Int Y) & Y c= X & Y is compact;

    end

    registration

      cluster compact T_2 -> regular normal locally-compact for non empty TopSpace;

      coherence

      proof

        let T be non empty TopSpace;

        assume

         A1: T is compact T_2;

        hence

         A2: T is regular & T is normal by COMPTS_1: 12, COMPTS_1: 13;

        

         A3: ( [#] T) is compact by A1;

        let x be Point of T, X be Subset of T;

        assume that

         A4: x in X and

         A5: X is open;

        consider Y be open Subset of T such that

         A6: x in Y and

         A7: ( Cl Y) c= X by A2, A4, A5, URYSOHN1: 21;

        take Z = ( Cl Y);

        Y c= ( Int Z) by PRE_TOPC: 18, TOPS_1: 24;

        hence thesis by A3, A6, A7, COMPTS_1: 9;

      end;

    end

    registration

      cluster compact T_2 for non empty TopSpace;

      existence

      proof

        take ( 1TopSp { 0 });

        thus thesis;

      end;

    end

    theorem :: WAYBEL_3:38

    

     Th38: for T be non empty TopSpace holds for x,y be Element of ( InclPoset the topology of T) st ex Z be Subset of T st x c= Z & Z c= y & Z is compact holds x << y

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      let x,y be Element of L;

      given Z be Subset of T such that

       A1: x c= Z and

       A2: Z c= y and

       A3: Z is compact;

      

       A4: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      then

       A5: x in the topology of T;

      y in the topology of T by A4;

      then

      reconsider X = x, Y = y as Subset of T by A5;

      let D be non empty directed Subset of L;

      

       A6: ( sup D) = ( union D) by YELLOW_1: 22;

      reconsider F = D as Subset-Family of T by A4, XBOOLE_1: 1;

      reconsider F as Subset-Family of T;

      

       A7: F is open

      proof

        let a be Subset of T;

        assume a in F;

        hence a in the topology of T by A4;

      end;

      assume y <= ( sup D);

      then Y c= ( union F) by A6, YELLOW_1: 3;

      then Z c= ( union F) by A2;

      then F is Cover of Z by SETFAM_1:def 11;

      then

      consider G be Subset-Family of T such that

       A8: G c= F and

       A9: G is Cover of Z and

       A10: G is finite by A3, A7;

      consider d be Element of L such that

       A11: d in D and

       A12: d is_>=_than G by A8, A10, WAYBEL_0: 1;

      take d;

      thus d in D by A11;

       A13:

      now

        let B be set;

        assume

         A14: B in G;

        then B in D by A8;

        then

        reconsider e = B as Element of L;

        d >= e by A12, A14;

        hence B c= d by YELLOW_1: 3;

      end;

      

       A15: Z c= ( union G) by A9, SETFAM_1:def 11;

      ( union G) c= d by A13, ZFMISC_1: 76;

      then Z c= d by A15;

      then X c= d by A1;

      hence thesis by YELLOW_1: 3;

    end;

    theorem :: WAYBEL_3:39

    

     Th39: for T be non empty TopSpace st T is locally-compact holds for x,y be Element of ( InclPoset the topology of T) st x << y holds ex Z be Subset of T st x c= Z & Z c= y & Z is compact

    proof

      let T be non empty TopSpace such that

       A1: for x be Point of T, X be Subset of T st x in X & X is open holds ex Y be Subset of T st x in ( Int Y) & Y c= X & Y is compact;

      set L = ( InclPoset the topology of T);

      

       A2: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      let x,y be Element of L such that

       A3: x << y;

      

       A4: x in the topology of T by A2;

      y in the topology of T by A2;

      then

      reconsider X = x, Y = y as Subset of T by A4;

      

       A5: Y is open by A2;

      set VV = { ( Int Z) where Z be Subset of T : Z c= Y & Z is compact };

      reconsider e = ( {} T) as Subset of T;

      

       A6: {} c= Y;

      ( Int ( {} T)) = {} ;

      then

       A7: e in VV by A6;

      VV c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in VV;

        then ex Z be Subset of T st a = ( Int Z) & Z c= Y & Z is compact;

        hence thesis;

      end;

      then

      reconsider VV as non empty Subset-Family of T by A7;

      set V = ( union VV);

      VV is open

      proof

        let a be Subset of T;

        assume a in VV;

        then ex Z be Subset of T st a = ( Int Z) & Z c= Y & Z is compact;

        hence thesis;

      end;

      then

      reconsider A = VV as Subset of L by YELLOW_1: 25;

      

       A8: ( sup A) = V by YELLOW_1: 22;

      Y c= V

      proof

        let a be object;

        assume

         A9: a in Y;

        then

        reconsider a as Point of T;

        consider Z be Subset of T such that

         A10: a in ( Int Z) and

         A11: Z c= Y and

         A12: Z is compact by A1, A5, A9;

        ( Int Z) in VV by A11, A12;

        hence thesis by A10, TARSKI:def 4;

      end;

      then y <= ( sup A) by A8, YELLOW_1: 3;

      then

      consider B be finite Subset of L such that

       A13: B c= A and

       A14: x <= ( sup B) by A3, Th18;

      defpred P[ object, object] means ex Z be Subset of T st $2 = Z & $1 = ( Int Z) & Z c= Y & Z is compact;

       A15:

      now

        let z be object;

        assume z in B;

        then z in A by A13;

        then

        consider Z be Subset of T such that

         A16: z = ( Int Z) and

         A17: Z c= Y and

         A18: Z is compact;

        reconsider s = Z as object;

        take s;

        thus P[z, s] by A16, A17, A18;

      end;

      consider f be Function such that

       A19: ( dom f) = B and

       A20: for z be object st z in B holds P[z, (f . z)] from CLASSES1:sch 1( A15);

      reconsider W = B as Subset-Family of T by A2, XBOOLE_1: 1;

      ( sup B) = ( union W) by YELLOW_1: 22;

      then

       A21: X c= ( union W) by A14, YELLOW_1: 3;

      now

        let z be set;

        assume z in ( rng f);

        then

        consider a be object such that

         A22: a in B and

         A23: z = (f . a) by A19, FUNCT_1:def 3;

        ex Z be Subset of T st z = Z & a = ( Int Z) & Z c= Y & Z is compact by A20, A22, A23;

        hence z c= the carrier of T;

      end;

      then

      reconsider Z = ( union ( rng f)) as Subset of T by ZFMISC_1: 76;

      take Z;

      thus x c= Z

      proof

        let z be object;

        assume z in x;

        then

        consider a be set such that

         A24: z in a and

         A25: a in W by A21, TARSKI:def 4;

        consider Z be Subset of T such that

         A26: (f . a) = Z and

         A27: a = ( Int Z) and Z c= Y and Z is compact by A20, A25;

        

         A28: ( Int Z) c= Z by TOPS_1: 16;

        Z in ( rng f) by A19, A25, A26, FUNCT_1:def 3;

        hence thesis by A24, A27, A28, TARSKI:def 4;

      end;

      thus Z c= y

      proof

        let z be object;

        assume z in Z;

        then

        consider a be set such that

         A29: z in a and

         A30: a in ( rng f) by TARSKI:def 4;

        consider Z be object such that

         A31: Z in W and

         A32: a = (f . Z) by A19, A30, FUNCT_1:def 3;

        ex S be Subset of T st a = S & Z = ( Int S) & S c= Y & S is compact by A20, A31, A32;

        hence thesis by A29;

      end;

      

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

      defpred P[ set] means ex A be Subset of T st A = ( union $1) & A is compact;

      ( union {} ) = ( {} T) by ZFMISC_1: 2;

      then

       A34: P[ {} ];

       A35:

      now

        let x,B be set;

        assume that

         A36: x in ( rng f) and B c= ( rng f);

        assume P[B];

        then

        consider A be Subset of T such that

         A37: A = ( union B) and

         A38: A is compact;

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

        proof

          consider Z be object such that

           A39: Z in W and

           A40: x = (f . Z) by A19, A36, FUNCT_1:def 3;

          consider S be Subset of T such that

           A41: x = S and Z = ( Int S) and S c= Y and

           A42: S is compact by A20, A39, A40;

          reconsider Bx = (A \/ S) as Subset of T;

          take Bx;

          

          thus Bx = (( union B) \/ ( union {x})) by A37, A41, ZFMISC_1: 25

          .= ( union (B \/ {x})) by ZFMISC_1: 78;

          thus thesis by A38, A42, COMPTS_1: 10;

        end;

      end;

       P[( rng f)] from FINSET_1:sch 2( A33, A34, A35);

      hence thesis;

    end;

    theorem :: WAYBEL_3:40

    for T be non empty TopSpace st T is locally-compact & T is T_2 holds for x,y be Element of ( InclPoset the topology of T) st x << y holds ex Z be Subset of T st Z = x & ( Cl Z) c= y & ( Cl Z) is compact

    proof

      let T be non empty TopSpace such that

       A1: T is locally-compact and

       A2: T is T_2;

      set L = ( InclPoset the topology of T);

      

       A3: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      let x,y be Element of L;

      assume x << y;

      then

      consider Z be Subset of T such that

       A4: x c= Z and

       A5: Z c= y and

       A6: Z is compact by A1, Th39;

      x in the topology of T by A3;

      then

      reconsider X = x as Subset of T;

      take X;

      thus X = x;

      ( Cl X) c= Z by A2, A4, A6, TOPS_1: 5;

      hence thesis by A5, A6, COMPTS_1: 9;

    end;

    theorem :: WAYBEL_3:41

    for X be non empty TopSpace st X is regular & ( InclPoset the topology of X) is continuous holds X is locally-compact

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      

       A1: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

      assume that

       A2: T is regular and

       A3: L is continuous;

      let x be Point of T, X be Subset of T;

      assume that

       A4: x in X and

       A5: X is open;

      reconsider a = X as Element of L by A1, A5;

      a = ( sup ( waybelow a)) by A3, Def5

      .= ( union ( waybelow a)) by YELLOW_1: 22;

      then

      consider Y be set such that

       A6: x in Y and

       A7: Y in ( waybelow a) by A4, TARSKI:def 4;

      Y in the carrier of L by A7;

      then

      reconsider Y as Subset of T by A1;

      consider y be Element of L such that

       A8: Y = y and

       A9: y << a by A7;

      Y is open by A1, A7;

      then

      consider W be open Subset of T such that

       A10: x in W and

       A11: ( Cl W) c= Y by A2, A6, URYSOHN1: 21;

      take Z = ( Cl W);

      W c= Z by PRE_TOPC: 18;

      hence x in ( Int Z) by A10, TOPS_1: 22;

      y <= a by A9, Th1;

      then Y c= X by A8, YELLOW_1: 3;

      hence Z c= X by A11;

      let F be Subset-Family of T such that

       A12: F is Cover of Z and

       A13: F is open;

      reconsider ZZ = {(Z ` )} as Subset-Family of T;

      reconsider ZZ as Subset-Family of T;

      reconsider FZ = (F \/ ZZ) as Subset-Family of T;

      for x be Subset of T st x in ZZ holds x is open by TARSKI:def 1;

      then ZZ is open;

      then FZ is open by A13, TOPS_2: 13;

      then

      reconsider FF = FZ as Subset of L by YELLOW_1: 25;

      

       A14: ( sup FF) = ( union FZ) by YELLOW_1: 22

      .= (( union F) \/ ( union ZZ)) by ZFMISC_1: 78

      .= (( union F) \/ (Z ` )) by ZFMISC_1: 25;

      Z c= ( union F) by A12, SETFAM_1:def 11;

      then (Z \/ (Z ` )) c= ( sup FF) by A14, XBOOLE_1: 9;

      then ( [#] T) c= ( sup FF) by PRE_TOPC: 2;

      then X c= ( sup FF);

      then a <= ( sup FF) by YELLOW_1: 3;

      then

      consider A be finite Subset of L such that

       A15: A c= FF and

       A16: y <= ( sup A) by A9, Th18;

      

       A17: ( sup A) = ( union A) by YELLOW_1: 22;

      reconsider G = (A \ ZZ) as Subset-Family of T by A1, XBOOLE_1: 1;

      take G;

      thus G c= F by A15, XBOOLE_1: 43;

      thus Z c= ( union G)

      proof

        let z be object;

        assume

         A18: z in Z;

        then

         A19: z in Y by A11;

        

         A20: Y c= ( union A) by A8, A16, A17, YELLOW_1: 3;

        

         A21: not z in (Z ` ) by A18, XBOOLE_0:def 5;

        consider B be set such that

         A22: z in B and

         A23: B in A by A19, A20, TARSKI:def 4;

         not B in ZZ by A21, A22, TARSKI:def 1;

        then B in G by A23, XBOOLE_0:def 5;

        hence thesis by A22, TARSKI:def 4;

      end;

      thus thesis;

    end;

    theorem :: WAYBEL_3:42

    for T be non empty TopSpace st T is locally-compact holds ( InclPoset the topology of T) is continuous

    proof

      let T be non empty TopSpace such that

       A1: T is locally-compact;

      set L = ( InclPoset the topology of T);

      

       A2: L = RelStr (# the topology of T, ( RelIncl the topology of T) #) by YELLOW_1:def 1;

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

      thus L is up-complete;

      let x be Element of L;

      x in the topology of T by A2;

      then

      reconsider X = x as Subset of T;

      thus x c= ( sup ( waybelow x))

      proof

        let a be object;

        assume

         A3: a in x;

        X is open by A2;

        then

        consider Y be Subset of T such that

         A4: a in ( Int Y) and

         A5: Y c= X and

         A6: Y is compact by A1, A3;

        reconsider iY = ( Int Y) as Subset of T;

        reconsider y = iY as Element of L by A2, PRE_TOPC:def 2;

        y << x by A5, A6, Th38, TOPS_1: 16;

        then y in ( waybelow x);

        then y c= ( union ( waybelow x)) by ZFMISC_1: 74;

        then y c= ( sup ( waybelow x)) by YELLOW_1: 22;

        hence thesis by A4;

      end;

      let a be object;

      assume a in ( sup ( waybelow x));

      then a in ( union ( waybelow x)) by YELLOW_1: 22;

      then

      consider Y be set such that

       A7: a in Y and

       A8: Y in ( waybelow x) by TARSKI:def 4;

      consider y be Element of L such that

       A9: Y = y and

       A10: y << x by A8;

      y <= x by A10, Th1;

      then Y c= x by A9, YELLOW_1: 3;

      hence thesis by A7;

    end;