poset_1.miz



    begin

    registration

      let P be non empty Poset;

      cluster non empty for Chain of P;

      existence

      proof

        ex L be Chain of P st L is non empty

        proof

          set z = the Element of P;

          set IT = {z};

          reconsider IT as Chain of P by ORDERS_2: 8;

          IT is non empty;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let IT be RelStr;

      :: POSET_1:def1

      attr IT is chain-complete means

      : Def1: IT is lower-bounded & for L be Chain of IT st L is non empty holds ex_sup_of (L,IT);

    end

    theorem :: POSET_1:1

    

     Th1: for P1,P2 be non empty Poset, K be non empty Chain of P1, h be monotone Function of P1, P2 holds (h .: K) is non empty Chain of P2

    proof

      let P1,P2 be non empty Poset, K be non empty Chain of P1, h be monotone Function of P1, P2;

      set R = the InternalRel of P2;

      set K2 = (h .: K);

      for x,y be object st x in K2 & y in K2 & x <> y holds [x, y] in R or [y, x] in R

      proof

        let x,y be object;

        assume

         A1: x in K2 & y in K2 & x <> y;

        then

        reconsider x, y as Element of P2;

        consider a be object such that

         A2: a in ( dom h) & a in K & x = (h . a) by A1, FUNCT_1:def 6;

        consider b be object such that

         A3: b in ( dom h) & b in K & y = (h . b) by A1, FUNCT_1:def 6;

        reconsider a, b as Element of P1 by A2, A3;

        a <= b or b <= a by A2, A3, ORDERS_2: 11;

        then x <= y or y <= x by A2, A3, ORDERS_3:def 5;

        hence thesis by ORDERS_2:def 5;

      end;

      then

       A4: R is_connected_in K2 by RELAT_2:def 6;

      for x be object st x in K2 holds [x, x] in R

      proof

        let x be object;

        assume x in K2;

        then

        reconsider x as Element of P2;

        x <= x;

        hence thesis by ORDERS_2:def 5;

      end;

      then R is_reflexive_in K2 by RELAT_2:def 1;

      then R is_strongly_connected_in K2 by A4, ORDERS_1: 7;

      then

      reconsider K2 as Chain of P2 by ORDERS_2:def 7;

      consider a be object such that

       A5: a in K by XBOOLE_0: 7;

      a in the carrier of P1 by A5;

      then a in ( dom h) by FUNCT_2:def 1;

      then (h . a) in K2 by A5, FUNCT_1:def 6;

      hence thesis;

    end;

    registration

      cluster strict chain-complete non empty for Poset;

      existence

      proof

        set z = the set;

        set A = {z};

        reconsider R = ( id A) as Relation of A;

        reconsider R as Order of A;

        take IT = RelStr (# A, R #);

        reconsider z as Element of IT by TARSKI:def 1;

        for L be Chain of IT st L is non empty holds ex_sup_of (L,IT)

        proof

          let L be Chain of IT;

          assume L is non empty;

          for x be Element of IT st x in L holds x <= z by TARSKI:def 1;

          then

           A1: L is_<=_than z;

          for y be Element of IT holds L is_<=_than y implies z <= y by TARSKI:def 1;

          hence thesis by A1, YELLOW_0: 15;

        end;

        hence thesis;

      end;

    end

    registration

      cluster chain-complete -> lower-bounded for RelStr;

      coherence ;

    end

    reserve n,m,k for Nat;

    reserve x,y,z,X for set;

    reserve P,Q for strict chain-complete non empty Poset;

    reserve L for non empty Chain of P;

    reserve M for non empty Chain of Q;

    reserve p,p1,p2,p3,p4 for Element of P;

    reserve q,q1,q2 for Element of Q;

    reserve f for monotone Function of P, Q;

    reserve g,g1,g2 for monotone Function of P, P;

    theorem :: POSET_1:2

    

     Th2: ( sup (f .: L)) <= (f . ( sup L))

    proof

      reconsider M = (f .: L) as non empty Chain of Q by Th1;

      set r = ( sup L);

      set u = (f . ( sup L));

      

       A1: ex_sup_of (L,P) & ex_sup_of (M,Q) by Def1;

      for q st q in M holds q <= u

      proof

        let q;

        assume q in M;

        then

        consider x be object such that

         A2: x in ( dom f) & x in L & q = (f . x) by FUNCT_1:def 6;

        reconsider x as Element of P by A2;

        L is_<=_than r by A1, YELLOW_0:def 9;

        then x <= r by A2;

        hence thesis by A2, ORDERS_3:def 5;

      end;

      then M is_<=_than u;

      hence thesis by A1, YELLOW_0:def 9;

    end;

    begin

    

     Lm1: for P be non empty Poset, g be monotone Function of P, P, p be Element of P holds (( iter (g, 0 )) . p) = p

    proof

      let P be non empty Poset, g be monotone Function of P, P, p be Element of P;

      set X = the carrier of P;

      (( iter (g, 0 )) . p) = (( id X) . p) by FUNCT_7: 84

      .= p;

      hence thesis;

    end;

    definition

      let P be non empty Poset, g be monotone Function of P, P, p be Element of P;

      :: POSET_1:def2

      func iterSet (g,p) -> non empty set equals { x where x be Element of P : ex n be Nat st x = (( iter (g,n)) . p) };

      correctness

      proof

        set IT = { x where x be Element of P : ex n be Nat st x = (( iter (g,n)) . p) };

        IT is non empty

        proof

          (( iter (g, 0 )) . p) = p by Lm1;

          then p in IT;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    

     Lm2: ((g * ( iter (g,n))) . p) = (g . (( iter (g,n)) . p)) & ((( iter (g,n)) * g) . p) = (( iter (g,n)) . (g . p)) by FUNCT_2: 15;

    

     Lm3: p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,n)) . p3) implies p1 <= p4

    proof

      defpred U[ Nat] means for p, p3, p1, p4 holds p <= p3 & p1 = (( iter (g,$1)) . p) & p4 = (( iter (g,$1)) . p3) implies p1 <= p4;

      

       A1: U[ 0 ]

      proof

        let p, p3, p1, p4;

        assume p <= p3 & p1 = (( iter (g, 0 )) . p) & p4 = (( iter (g, 0 )) . p3);

        then p <= p3 & p1 = p & p4 = p3 by Lm1;

        hence thesis;

      end;

      

       A2: U[k] implies U[(k + 1)]

      proof

        assume

         A3: for p, p3, p1, p4 holds p <= p3 & p1 = (( iter (g,k)) . p) & p4 = (( iter (g,k)) . p3) implies p1 <= p4;

         U[(k + 1)]

        proof

          let p, p3, p1, p4;

          assume

           A4: p <= p3 & p1 = (( iter (g,(k + 1))) . p) & p4 = (( iter (g,(k + 1))) . p3);

          reconsider x1 = (( iter (g,k)) . p) as Element of P;

          reconsider y1 = (( iter (g,k)) . p3) as Element of P;

          

           A5: x1 <= y1 by A4, A3;

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

          then p1 = (g . (( iter (g,k)) . p)) & p4 = (g . (( iter (g,k)) . p3)) by Lm2, A4;

          hence thesis by A5, ORDERS_3:def 5;

        end;

        hence thesis;

      end;

       U[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm4: p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,(n + k))) . p) implies p1 <= p4

    proof

      defpred U[ Nat] means for p, p3, p1, p4 holds p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,(n + $1))) . p) implies p1 <= p4;

      

       A1: U[ 0 ];

      

       A2: for k be Nat st U[k] holds U[(k + 1)]

      proof

        let k;

        assume

         A3: for p, p3, p1, p4 holds p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,(n + k))) . p) implies p1 <= p4;

         U[(k + 1)]

        proof

          let p, p3, p1, p4;

          assume

           A4: p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,(n + (k + 1)))) . p);

          reconsider y1 = (( iter (g,(n + k))) . p) as Element of P;

          

           A5: p1 <= y1 by A4, A3;

          ( iter (g,(n + (k + 1)))) = ( iter (g,((n + k) + 1)))

          .= (( iter (g,(n + k))) * g) by FUNCT_7: 69;

          then p4 = (( iter (g,(n + k))) . p3) by Lm2, A4;

          then y1 <= p4 by A4, Lm3;

          hence thesis by A5, ORDERS_2: 3;

        end;

        hence thesis;

      end;

      for k be Nat holds U[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm5: n <= m & p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,m)) . p) implies p1 <= p4

    proof

      assume

       A1: n <= m & p3 = (g . p) & p <= p3 & p1 = (( iter (g,n)) . p) & p4 = (( iter (g,m)) . p);

      then

      consider k such that

       A2: m = (n + k) by NAT_1: 10;

      thus thesis by A1, A2, Lm4;

    end;

    

     Lm6: p is_a_fixpoint_of g implies (( iter (g,n)) . p) = p

    proof

      defpred U[ Nat] means for p holds p is_a_fixpoint_of g implies (( iter (g,$1)) . p) = p;

      

       A1: U[ 0 ] by Lm1;

      

       A2: for k be Nat st U[k] holds U[(k + 1)]

      proof

        let k;

        assume

         A3: U[k];

         U[(k + 1)]

        proof

          let p;

          assume

           A4: p is_a_fixpoint_of g;

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

          

          then (( iter (g,(k + 1))) . p) = (g . (( iter (g,k)) . p)) by Lm2

          .= (g . p) by A4, A3

          .= p by A4, ABIAN:def 3;

          hence thesis;

        end;

        hence thesis;

      end;

      for k be Nat holds U[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm7: g1 <= g2 & p1 = (( iter (g1,n)) . p) & p2 = (( iter (g2,n)) . p) implies p1 <= p2

    proof

      defpred U[ Nat] means for p, p1, p2 holds g1 <= g2 & p1 = (( iter (g1,$1)) . p) & p2 = (( iter (g2,$1)) . p) implies p1 <= p2;

      

       A1: U[ 0 ]

      proof

        let p, p1, p2;

        assume g1 <= g2 & p1 = (( iter (g1, 0 )) . p) & p2 = (( iter (g2, 0 )) . p);

        then p1 = p & p2 = p by Lm1;

        hence thesis;

      end;

      

       A2: for k be Nat st U[k] holds U[(k + 1)]

      proof

        let k;

        assume

         A3: U[k];

         U[(k + 1)]

        proof

          let p, p1, p2;

          assume

           A4: g1 <= g2 & p1 = (( iter (g1,(k + 1))) . p) & p2 = (( iter (g2,(k + 1))) . p);

          reconsider q1 = (( iter (g1,k)) . p) as Element of P;

          reconsider q2 = (( iter (g2,k)) . p) as Element of P;

          set r = (g1 . q2);

          

           A5: q1 <= q2 by A4, A3;

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

          then

           A6: p1 = (g1 . q1) by Lm2, A4;

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

          then

           A7: p2 = (g2 . q2) by Lm2, A4;

          

           A8: p1 <= r by A5, A6, ORDERS_3:def 5;

          r <= p2 by A4, A7, YELLOW_2: 9;

          hence thesis by A8, ORDERS_2: 3;

        end;

        hence thesis;

      end;

      for k be Nat holds U[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: POSET_1:3

    

     Th3: ( iterSet (g,( Bottom P))) is non empty Chain of P

    proof

      set a = ( Bottom P);

      set R = the InternalRel of P;

      set L = ( iterSet (g,a));

      

       A1: x in L implies x is Element of P

      proof

        assume x in L;

        then

        consider y be Element of P such that

         A2: x = y & ex n be Nat st y = (( iter (g,n)) . a);

        thus thesis by A2;

      end;

      for x be object holds x in L implies x in the carrier of P

      proof

        let x be object;

        assume x in L;

        then x is Element of the carrier of P by A1;

        hence thesis;

      end;

      then

      reconsider L as Subset of P by TARSKI:def 3;

      for x,y be object holds x in L & y in L & x <> y implies [x, y] in R or [y, x] in R

      proof

        let x,y be object;

        assume

         A3: x in L & y in L & x <> y;

        then

        reconsider x, y as Element of P;

        consider p such that

         A4: x = p & ex n st p = (( iter (g,n)) . a) by A3;

        consider p1 such that

         A5: y = p1 & ex m st p1 = (( iter (g,m)) . a) by A3;

        consider n such that

         A6: p = (( iter (g,n)) . a) by A4;

        consider m such that

         A7: p1 = (( iter (g,m)) . a) by A5;

        p <= p1 or p1 <= p

        proof

          set a1 = (( iter (g,1)) . a);

          

           A8: a1 = (g . a) by FUNCT_7: 70;

          per cases ;

            suppose n <= m;

            hence thesis by A6, A7, A8, Lm5, YELLOW_0: 44;

          end;

            suppose m <= n;

            hence thesis by A6, A7, A8, Lm5, YELLOW_0: 44;

          end;

        end;

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

      end;

      then

       A9: R is_connected_in L by RELAT_2:def 6;

      for x be object holds x in L implies [x, x] in R

      proof

        let x be object;

        assume x in L;

        then

        reconsider x as Element of P;

        x <= x;

        hence thesis by ORDERS_2:def 5;

      end;

      then R is_reflexive_in L by RELAT_2:def 1;

      then R is_strongly_connected_in L by A9, ORDERS_1: 7;

      then

      reconsider L as Chain of P by ORDERS_2:def 7;

      L is non empty Chain of P;

      hence thesis;

    end;

    definition

      let P;

      let g be monotone Function of P, P;

      :: POSET_1:def3

      func iter_min (g) -> non empty Chain of P equals ( iterSet (g,( Bottom P)));

      correctness by Th3;

    end

    theorem :: POSET_1:4

    

     Th4: ( sup ( iter_min g)) = ( sup (g .: ( iter_min g)))

    proof

      reconsider L = (g .: ( iter_min g)) as non empty Chain of P by Th1;

      

       A1: ex_sup_of (( iter_min g),P) & ex_sup_of (L,P) by Def1;

      set a = ( Bottom P);

      set s1 = ( sup ( iter_min g));

      set s2 = ( sup L);

      

       A2: ( iter_min g) is_<=_than s1 by A1, YELLOW_0:def 9;

      

       A3: L is_<=_than s2 by A1, YELLOW_0:def 9;

      for x be Element of P st x in ( iter_min g) holds x <= s2

      proof

        let x be Element of P;

        assume x in ( iter_min g);

        then

        consider p such that

         A4: x = p & ex n st p = (( iter (g,n)) . a);

        consider n such that

         A5: p = (( iter (g,n)) . a) by A4;

        

         A6: 1 <= n implies p in L

        proof

          assume 1 <= n;

          then

          consider k such that

           A7: n = (1 + k) by NAT_1: 10;

          reconsider z = (( iter (g,k)) . a) as Element of P;

          z in the carrier of P;

          then

           A8: z in ( dom g) & z in ( iter_min g) by FUNCT_2:def 1;

          p = ((g * ( iter (g,k))) . a) by A5, A7, FUNCT_7: 71

          .= (g . z) by Lm2;

          hence thesis by A8, FUNCT_1:def 6;

        end;

        n = 0 implies p = a by A5, Lm1;

        hence thesis by A6, A4, A3, NAT_1: 14, YELLOW_0: 44;

      end;

      then ( iter_min g) is_<=_than s2;

      then

       A9: s1 <= s2 by A1, YELLOW_0: 30;

      for x be Element of P st x in L holds x <= s1

      proof

        let x be Element of P;

        assume x in L;

        then

        consider z be object such that

         A10: z in ( dom g) & z in ( iter_min g) & x = (g . z) by FUNCT_1:def 6;

        consider z1 be Element of P such that

         A11: z = z1 & ex n st z1 = (( iter (g,n)) . a) by A10;

        consider n such that

         A12: z1 = (( iter (g,n)) . a) by A11;

        set n1 = (n + 1);

        (g . z) = ((g * ( iter (g,n))) . a) by Lm2, A11, A12

        .= (( iter (g,n1)) . a) by FUNCT_7: 71;

        then x in ( iterSet (g,a)) by A10;

        hence thesis by A2;

      end;

      then L is_<=_than s1;

      then s2 <= s1 by A1, YELLOW_0:def 9;

      hence thesis by A9, ORDERS_2: 2;

    end;

    theorem :: POSET_1:5

    

     Th5: g1 <= g2 implies ( sup ( iter_min g1)) <= ( sup ( iter_min g2))

    proof

      assume

       A1: g1 <= g2;

      set p2 = ( sup ( iter_min g2));

      set a = ( Bottom P);

      

       A2: ex_sup_of (( iter_min g1),P) & ex_sup_of (( iter_min g2),P) by Def1;

      then

       A3: ( iter_min g2) is_<=_than p2 by YELLOW_0:def 9;

      for x be Element of P st x in ( iter_min g1) holds x <= p2

      proof

        let x be Element of P;

        assume x in ( iter_min g1);

        then

        consider p such that

         A4: x = p & ex n st p = (( iter (g1,n)) . a);

        consider n such that

         A5: p = (( iter (g1,n)) . a) by A4;

        reconsider y = (( iter (g2,n)) . a) as Element of P;

        y in ( iter_min g2);

        then

         A6: y <= p2 by A3;

        p <= y by A1, A5, Lm7;

        hence thesis by A4, A6, ORDERS_2: 3;

      end;

      then ( iter_min g1) is_<=_than p2;

      hence thesis by A2, YELLOW_0: 30;

    end;

    definition

      let P,Q be non empty Poset;

      let f be Function of P, Q;

      :: POSET_1:def4

      attr f is continuous means f is monotone & for L be non empty Chain of P holds f preserves_sup_of L;

    end

    theorem :: POSET_1:6

    

     Th6: for f be Function of P, Q holds f is continuous iff (f is monotone & for L holds (f . ( sup L)) = ( sup (f .: L)))

    proof

      let f be Function of P, Q;

      thus f is continuous implies (f is monotone & for L holds (f . ( sup L)) = ( sup (f .: L)))

      proof

        assume

         A1: f is continuous;

        for L holds (f . ( sup L)) = ( sup (f .: L))

        proof

          let L;

          

           A2: f preserves_sup_of L by A1;

           ex_sup_of (L,P) by Def1;

          hence thesis by A2, WAYBEL_0:def 31;

        end;

        hence thesis by A1;

      end;

      assume that

       A3: f is monotone and

       A4: for L holds (f . ( sup L)) = ( sup (f .: L));

      for L holds f preserves_sup_of L

      proof

        let L;

        reconsider M = (f .: L) as non empty Chain of Q by A3, Th1;

         ex_sup_of (M,Q) & (f . ( sup L)) = ( sup M) by Def1, A4;

        hence thesis by WAYBEL_0:def 31;

      end;

      hence thesis by A3;

    end;

    theorem :: POSET_1:7

    

     Th7: for z be Element of Q holds (P --> z) is continuous

    proof

      let z be Element of Q;

      set IT = (P --> z);

      for L holds (IT . ( sup L)) = ( sup (IT .: L))

      proof

        let L;

        set M = (IT .: L);

        for x be Element of Q st x in M holds x <= z

        proof

          let x be Element of Q;

          assume x in M;

          then

          consider a be object such that

           A1: a in ( dom IT) & a in L & x = (IT . a) by FUNCT_1:def 6;

          thus thesis by A1, FUNCOP_1: 7;

        end;

        then

         A2: M is_<=_than z;

        for y be Element of Q st M is_<=_than y holds z <= y

        proof

          let y be Element of Q;

          assume

           A3: M is_<=_than y;

          consider a be object such that

           A4: a in L by XBOOLE_0:def 1;

          a in the carrier of P by A4;

          then

           A5: a in ( dom IT) by FUNCOP_1: 13;

          (IT . a) = z by A4, FUNCOP_1: 7;

          then z in M by A4, A5, FUNCT_1:def 6;

          hence thesis by A3;

        end;

        then z = ( "\/" (M,Q)) by A2, YELLOW_0: 30;

        hence thesis by FUNCOP_1: 7;

      end;

      hence thesis by Th6;

    end;

    registration

      let P, Q;

      cluster continuous for Function of P, Q;

      existence

      proof

        set z = the Element of Q;

        take (P --> z);

        thus thesis by Th7;

      end;

    end

    registration

      let P, Q;

      cluster continuous -> monotone for Function of P, Q;

      correctness ;

    end

    theorem :: POSET_1:8

    

     Th8: for f be monotone Function of P, Q holds (for L holds (f . ( sup L)) <= ( sup (f .: L))) implies f is continuous

    proof

      let f be monotone Function of P, Q;

      assume

       A1: for L holds (f . ( sup L)) <= ( sup (f .: L));

      for L holds (f . ( sup L)) = ( sup (f .: L))

      proof

        let L;

        set a1 = (f . ( sup L));

        set a2 = ( sup (f .: L));

        

         A2: a2 <= a1 by Th2;

        a1 <= a2 by A1;

        hence thesis by A2, ORDERS_2: 2;

      end;

      hence thesis by Th6;

    end;

    

     Lm8: g is continuous & p = ( sup ( iter_min g)) implies p is_a_fixpoint_of g

    proof

      

       A1: ( dom g) = the carrier of P by FUNCT_2:def 1;

      reconsider L = (g .: ( iter_min g)) as non empty Chain of P by Th1;

      assume

       A2: g is continuous & p = ( sup ( iter_min g));

      

      then (g . p) = ( sup L) by Th6

      .= p by A2, Th4;

      hence thesis by A1, ABIAN:def 3;

    end;

    

     Lm9: p4 = ( sup ( iter_min g)) implies for p st p is_a_fixpoint_of g holds p4 <= p

    proof

      assume

       A1: p4 = ( sup ( iter_min g));

      for p st p is_a_fixpoint_of g holds p4 <= p

      proof

        let p;

        assume

         A2: p is_a_fixpoint_of g;

        set M = ( iter_min g);

        set a = ( Bottom P);

        

         A3: ex_sup_of (M,P) by Def1;

        for p1 st p1 in M holds p1 <= p

        proof

          let p1;

          assume p1 in M;

          then

          consider p2 such that

           A4: p1 = p2 & ex n st p2 = (( iter (g,n)) . a);

          consider n such that

           A5: p1 = (( iter (g,n)) . a) by A4;

          reconsider q = (( iter (g,n)) . p) as Element of P;

          p1 <= q by A5, Lm3, YELLOW_0: 44;

          hence thesis by A2, Lm6;

        end;

        then M is_<=_than p;

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

      end;

      hence thesis;

    end;

    definition

      let P;

      let g be monotone Function of P, P;

      assume

       A1: g is continuous;

      :: POSET_1:def5

      func least_fix_point (g) -> Element of P means

      : Def5: it is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds it <= p;

      existence

      proof

        set IT = ( sup ( iter_min g));

        take IT;

        thus thesis by A1, Lm8, Lm9;

      end;

      uniqueness

      proof

        let p1, p2;

        assume (p1 is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds p1 <= p) & (p2 is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds p2 <= p);

        then p1 <= p2 & p2 <= p1;

        hence thesis by ORDERS_2: 2;

      end;

    end

    theorem :: POSET_1:9

    

     Th9: for g be continuous Function of P, P holds ( least_fix_point g) = ( sup ( iter_min g))

    proof

      let g be continuous Function of P, P;

      set p = ( sup ( iter_min g));

      set q = ( least_fix_point g);

      p is_a_fixpoint_of g by Lm8;

      then

       A1: q <= p by Def5;

      q is_a_fixpoint_of g by Def5;

      then p <= q by Lm9;

      hence thesis by A1, ORDERS_2: 2;

    end;

    theorem :: POSET_1:10

    

     Th10: for g1,g2 be continuous Function of P, P st g1 <= g2 holds ( least_fix_point g1) <= ( least_fix_point g2)

    proof

      let g1,g2 be continuous Function of P, P;

      assume

       A1: g1 <= g2;

      set p1 = ( sup ( iter_min g1));

      set p2 = ( sup ( iter_min g2));

      p1 = ( least_fix_point g1) & p2 = ( least_fix_point g2) by Th9;

      hence thesis by A1, Th5;

    end;

    begin

    definition

      let P, Q;

      :: POSET_1:def6

      func ConFuncs (P,Q) -> non empty set equals { x where x be Element of ( Funcs (the carrier of P,the carrier of Q)) : ex f be continuous Function of P, Q st f = x };

      correctness

      proof

        set IT = { x where x be Element of ( Funcs (the carrier of P,the carrier of Q)) : ex f be continuous Function of P, Q st f = x };

        IT is non empty

        proof

          set z = the Element of Q;

          reconsider f = (P --> z) as continuous Function of P, Q by Th7;

          f is Element of ( Funcs (the carrier of P,the carrier of Q)) by FUNCT_2: 8;

          then f in IT;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    

     Lm10: for f be Function of P, Q holds f <= f

    proof

      let f be Function of P, Q;

      for p holds (f . p) <= (f . p);

      hence thesis by YELLOW_2: 9;

    end;

    

     Lm11: for f,g,h be Function of P, Q st f <= g & g <= h holds f <= h

    proof

      let f,g,h be Function of P, Q;

      assume

       A1: f <= g & g <= h;

      for p holds (f . p) <= (h . p)

      proof

        let p;

        q = (f . p) & q2 = (h . p) implies q <= q2

        proof

          assume

           A2: q = (f . p) & q2 = (h . p);

          set q1 = (g . p);

          q <= q1 & q1 <= q2 by A2, A1, YELLOW_2: 9;

          hence thesis by ORDERS_2: 3;

        end;

        hence thesis;

      end;

      hence thesis by YELLOW_2: 9;

    end;

    

     Lm12: for f,g be Function of P, Q st f <= g & g <= f holds f = g

    proof

      let f,g be Function of P, Q;

      assume

       A1: f <= g & g <= f;

      for x be object st x in the carrier of P holds (f . x) = (g . x)

      proof

        let x be object;

        assume x in the carrier of P;

        then

        reconsider p = x as Element of P;

        set q1 = (f . p);

        set q2 = (g . p);

        

         A2: q1 <= q2 by A1, YELLOW_2: 9;

        q2 <= q1 by A1, YELLOW_2: 9;

        hence thesis by A2, ORDERS_2: 2;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    definition

      let P, Q;

      :: POSET_1:def7

      func ConRelat (P,Q) -> Relation of ( ConFuncs (P,Q)) means

      : Def7: for x, y holds [x, y] in it iff (x in ( ConFuncs (P,Q)) & y in ( ConFuncs (P,Q)) & ex f,g be Function of P, Q st x = f & y = g & f <= g);

      existence

      proof

        defpred U[ object, object] means ex f,g be Function of P, Q st $1 = f & $2 = g & f <= g;

        set X = ( ConFuncs (P,Q));

        consider IT be Relation of X, X such that

         A1: for x,y be object holds [x, y] in IT iff x in X & y in X & U[x, y] from RELSET_1:sch 1;

        take IT;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set X = ( ConFuncs (P,Q));

        let Y1,Y2 be Relation of X;

        defpred P1[ set, set] means $1 in X & $2 in X & ex f,g be Function of P, Q st $1 = f & $2 = g & f <= g;

        (for x, y holds ( [x, y] in Y1 iff P1[x, y]) & for x, y holds ( [x, y] in Y2 iff P1[x, y])) implies Y1 = Y2

        proof

          assume

           A2: for x, y holds ( [x, y] in Y1 iff P1[x, y]) & for x, y holds ( [x, y] in Y2 iff P1[x, y]);

          then

           A3: for x1 be Element of X, y1 be Element of X holds ( [x1, y1] in Y1 iff P1[x1, y1]);

          

           A4: for x be Element of X, y be Element of X holds [x, y] in Y2 iff P1[x, y] by A2;

          thus thesis from RELSET_1:sch 4( A3, A4);

        end;

        hence thesis;

      end;

    end

    

     Lm13: ( field ( ConRelat (P,Q))) c= ( ConFuncs (P,Q))

    proof

      (( ConFuncs (P,Q)) \/ ( ConFuncs (P,Q))) c= ( ConFuncs (P,Q));

      hence thesis by RELSET_1: 8;

    end;

    

     Lm14: ( ConRelat (P,Q)) is_reflexive_in ( ConFuncs (P,Q))

    proof

      set R = ( ConRelat (P,Q));

      for x be object holds x in ( ConFuncs (P,Q)) implies [x, x] in R

      proof

        let x be object;

        assume

         A1: x in ( ConFuncs (P,Q));

        then

        consider x1 be Element of ( Funcs (the carrier of P,the carrier of Q)) such that

         A2: x = x1 and

         A3: ex f be continuous Function of P, Q st f = x1;

        consider f be continuous Function of P, Q such that

         A4: f = x1 by A3;

        f <= f by Lm10;

        hence thesis by A1, A2, A4, Def7;

      end;

      hence thesis by RELAT_2:def 1;

    end;

    

     Lm15: ( ConRelat (P,Q)) is_transitive_in ( ConFuncs (P,Q))

    proof

      set X = ( ConFuncs (P,Q));

      set R = ( ConRelat (P,Q));

      for x,y,z be object holds x in X & y in X & z in X & [x, y] in R & [y, z] in R implies [x, z] in R

      proof

        let x,y,z be object;

        assume

         A1: x in X & y in X & z in X & [x, y] in R & [y, z] in R;

        then

        consider f,g be Function of P, Q such that

         A2: x = f & y = g & f <= g by Def7;

        consider g1,h be Function of P, Q such that

         A3: y = g1 & z = h & g1 <= h by A1, Def7;

        f <= h by A3, A2, Lm11;

        hence thesis by A1, A2, A3, Def7;

      end;

      hence thesis by RELAT_2:def 8;

    end;

    

     Lm16: ( ConRelat (P,Q)) is_antisymmetric_in ( ConFuncs (P,Q))

    proof

      set X = ( ConFuncs (P,Q));

      reconsider R = ( ConRelat (P,Q)) as Relation of ( ConFuncs (P,Q));

      for x,y be object holds x in X & y in X & [x, y] in R & [y, x] in R implies x = y

      proof

        let x,y be object;

        assume

         A1: x in X & y in X & [x, y] in R & [y, x] in R;

        then

        consider f,g be Function of P, Q such that

         A2: x = f & y = g & f <= g by Def7;

        consider g1,f1 be Function of P, Q such that

         A3: y = g1 & x = f1 & g1 <= f1 by A1, Def7;

        thus thesis by A2, A3, Lm12;

      end;

      hence thesis by RELAT_2:def 4;

    end;

    registration

      let P, Q;

      cluster ( ConRelat (P,Q)) -> reflexive;

      coherence

      proof

        ( ConRelat (P,Q)) is_reflexive_in ( field ( ConRelat (P,Q)))

        proof

          reconsider R = ( ConRelat (P,Q)) as Relation of ( ConFuncs (P,Q));

          for x be object holds x in ( field R) implies [x, x] in R

          proof

            let x be object;

            assume

             A1: x in ( field R);

            

             A2: ( field R) c= ( ConFuncs (P,Q)) by Lm13;

            R is_reflexive_in ( ConFuncs (P,Q)) by Lm14;

            hence thesis by A1, A2, RELAT_2:def 1;

          end;

          hence thesis by RELAT_2:def 1;

        end;

        hence thesis by RELAT_2:def 9;

      end;

      cluster ( ConRelat (P,Q)) -> transitive;

      coherence

      proof

        ( ConRelat (P,Q)) is_transitive_in ( field ( ConRelat (P,Q)))

        proof

          set X = ( field ( ConRelat (P,Q)));

          set R = ( ConRelat (P,Q));

          for x,y,z be object holds x in X & y in X & z in X & [x, y] in R & [y, z] in R implies [x, z] in R

          proof

            let x,y,z be object;

            assume

             A3: x in X & y in X & z in X & [x, y] in R & [y, z] in R;

            set X1 = ( ConFuncs (P,Q));

            

             A4: ( field R) c= X1 by Lm13;

            R is_transitive_in X1 by Lm15;

            hence thesis by A3, A4, RELAT_2:def 8;

          end;

          hence thesis by RELAT_2:def 8;

        end;

        hence thesis by RELAT_2:def 16;

      end;

      cluster ( ConRelat (P,Q)) -> antisymmetric;

      coherence

      proof

        ( ConRelat (P,Q)) is_antisymmetric_in ( field ( ConRelat (P,Q)))

        proof

          set X = ( field ( ConRelat (P,Q)));

          reconsider R = ( ConRelat (P,Q)) as Relation of ( ConFuncs (P,Q));

          for x,y be object holds x in X & y in X & [x, y] in R & [y, x] in R implies x = y

          proof

            let x,y be object;

            assume

             A5: x in X & y in X & [x, y] in R & [y, x] in R;

            set X1 = ( ConFuncs (P,Q));

            

             A6: ( field R) c= X1 by Lm13;

            R is_antisymmetric_in X1 by Lm16;

            hence thesis by A5, A6, RELAT_2:def 4;

          end;

          hence thesis by RELAT_2:def 4;

        end;

        hence thesis by RELAT_2:def 12;

      end;

    end

    definition

      let P, Q;

      :: POSET_1:def8

      func ConPoset (P,Q) -> strict non empty Poset equals RelStr (# ( ConFuncs (P,Q)), ( ConRelat (P,Q)) #);

      correctness by Lm14, Lm15, Lm16, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

    end

    reserve F for non empty Chain of ( ConPoset (P,Q));

    definition

      let P, Q, F, p;

      :: POSET_1:def9

      func F -image p -> non empty Chain of Q equals { x where x be Element of Q : ex f be continuous Function of P, Q st f in F & x = (f . p) };

      correctness

      proof

        set R = the InternalRel of Q;

        set IT = { x where x be Element of Q : ex f be continuous Function of P, Q st f in F & x = (f . p) };

        for x be object holds x in IT implies x in the carrier of Q

        proof

          let x be object;

          assume x in IT;

          then

          consider a be Element of Q such that

           A1: x = a & ex f be continuous Function of P, Q st f in F & a = (f . p);

          reconsider x as Element of the carrier of Q by A1;

          x in the carrier of Q;

          hence thesis;

        end;

        then

        reconsider IT as Subset of Q by TARSKI:def 3;

        for x,y be object holds x in IT & y in IT & x <> y implies [x, y] in R or [y, x] in R

        proof

          let x,y be object;

          assume

           A2: x in IT & y in IT & x <> y;

          then

          consider a be Element of Q such that

           A3: x = a & ex f be continuous Function of P, Q st f in F & a = (f . p);

          consider f be continuous Function of P, Q such that

           A4: f in F & a = (f . p) by A3;

          consider b be Element of Q such that

           A5: y = b & ex g be continuous Function of P, Q st g in F & b = (g . p) by A2;

          consider g be continuous Function of P, Q such that

           A6: g in F & b = (g . p) by A5;

          set S = the InternalRel of ( ConPoset (P,Q));

          

           A7: S is_strongly_connected_in F by ORDERS_2:def 7;

          per cases by A7, A4, A6, RELAT_2:def 7;

            suppose [f, g] in S;

            then

            consider f1,g1 be Function of P, Q such that

             A8: f = f1 & g = g1 & f1 <= g1 by Def7;

            a <= b by A8, A4, A6, YELLOW_2: 9;

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

          end;

            suppose [g, f] in S;

            then

            consider g1,f1 be Function of P, Q such that

             A9: g = g1 & f = f1 & g1 <= f1 by Def7;

            b <= a by A9, A4, A6, YELLOW_2: 9;

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

          end;

        end;

        then

         A10: R is_connected_in IT by RELAT_2:def 6;

        for x be object holds x in IT implies [x, x] in R

        proof

          let x be object;

          assume x in IT;

          then

          reconsider x as Element of Q;

          x <= x;

          hence thesis by ORDERS_2:def 5;

        end;

        then R is_reflexive_in IT by RELAT_2:def 1;

        then R is_strongly_connected_in IT by A10, ORDERS_1: 7;

        then

        reconsider IT as Chain of Q by ORDERS_2:def 7;

        consider a be object such that

         A11: a in F by XBOOLE_0: 7;

        a in ( ConFuncs (P,Q)) by A11;

        then

        consider b be Element of ( Funcs (the carrier of P,the carrier of Q)) such that

         A12: a = b & ex f be continuous Function of P, Q st f = b;

        consider f be continuous Function of P, Q such that

         A13: f = b by A12;

        reconsider c = (f . p) as Element of Q;

        c in IT by A11, A12, A13;

        hence thesis;

      end;

    end

    definition

      let P, Q, F;

      :: POSET_1:def10

      func sup_func (F) -> Function of P, Q means

      : Def10: for p, M holds M = (F -image p) implies (it . p) = ( sup M);

      existence

      proof

        set X = the carrier of P;

        set Y = the carrier of Q;

        defpred U[ object, object] means for p, M holds p = $1 & M = (F -image p) implies $2 = ( sup M);

        

         A1: for x be object st x in X holds ex y be object st y in Y & U[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider x as Element of P;

          reconsider a = (F -image x) as non empty Chain of Q;

          set y = ( sup a);

          take y;

          thus thesis;

        end;

        consider IT be Function of X, Y such that

         A2: for x be object st x in X holds U[x, (IT . x)] from FUNCT_2:sch 1( A1);

        for p, M holds M = (F -image p) implies (IT . p) = ( sup M) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of P, Q;

        (for p, M holds M = (F -image p) implies (f . p) = ( sup M)) & (for p, M holds M = (F -image p) implies (g . p) = ( sup M)) implies f = g

        proof

          assume

           A3: (for p, M holds M = (F -image p) implies (f . p) = ( sup M)) & (for p, M holds M = (F -image p) implies (g . p) = ( sup M));

          set X = the carrier of P;

          for x be object st x in X holds (f . x) = (g . x)

          proof

            let x be object;

            assume x in X;

            then

            reconsider p = x as Element of P;

            reconsider M = (F -image p) as non empty Chain of Q;

            (f . x) = ( sup M) by A3

            .= (g . x) by A3;

            hence thesis;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        hence thesis;

      end;

    end

    

     Lm17: ( sup_func F) is monotone

    proof

      reconsider f = ( sup_func F) as Function of P, Q;

      for p, p1 st p <= p1 holds for q, q1 st q = (f . p) & q1 = (f . p1) holds q <= q1

      proof

        let p, p1;

        assume

         A1: p <= p1;

        for q, q1 st q = (f . p) & q1 = (f . p1) holds q <= q1

        proof

          let q, q1;

          assume

           A2: q = (f . p) & q1 = (f . p1);

          reconsider X = (F -image p) as non empty Chain of Q;

          reconsider X1 = (F -image p1) as non empty Chain of Q;

          

           A3: ex_sup_of (X,Q) & ex_sup_of (X1,Q) by Def1;

          

           A4: q = ( sup X) by A2, Def10;

          q1 = ( sup X1) by A2, Def10;

          then

           A5: X1 is_<=_than q1 by A3, YELLOW_0:def 9;

          for x be Element of Q st x in X holds x <= q1

          proof

            let x be Element of Q;

            assume x in X;

            then

            consider a be Element of Q such that

             A6: x = a & ex g be continuous Function of P, Q st g in F & a = (g . p);

            consider g be continuous Function of P, Q such that

             A7: g in F & a = (g . p) by A6;

            reconsider b = (g . p1) as Element of Q;

            

             A8: a <= b by A1, A7, ORDERS_3:def 5;

            b in X1 by A7;

            then b <= q1 by A5;

            hence thesis by A6, A8, ORDERS_2: 3;

          end;

          then X is_<=_than q1;

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

        end;

        hence thesis;

      end;

      hence thesis by ORDERS_3:def 5;

    end;

    

     Lm18: q in M implies q <= ( sup M)

    proof

      assume

       A1: q in M;

      

       A2: ex_sup_of (M,Q) by Def1;

      set x = ( sup M);

      M is_<=_than x by A2, YELLOW_0:def 9;

      hence thesis by A1;

    end;

    

     Lm19: (for q st q in M holds q <= q1) implies ( sup M) <= q1

    proof

      assume for q st q in M holds q <= q1;

      then

       A1: M is_<=_than q1;

      

       A2: ex_sup_of (M,Q) by Def1;

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

    end;

    

     Lm20: ( sup_func F) is continuous

    proof

      reconsider f = ( sup_func F) as monotone Function of P, Q by Lm17;

      for L holds (f . ( sup L)) <= ( sup (f .: L))

      proof

        let L;

        reconsider M1 = (f .: L) as non empty Chain of Q by Th1;

        set q1 = ( sup M1);

        set a = ( sup L);

        set M = (F -image a);

        

         A1: (f . a) = ( sup M) by Def10;

        for q st q in M holds q <= q1

        proof

          let q;

          assume q in M;

          then

          consider q0 be Element of Q such that

           A2: q = q0 & ex g be continuous Function of P, Q st g in F & q0 = (g . a);

          consider g be continuous Function of P, Q such that

           A3: g in F & q0 = (g . a) by A2;

          reconsider M2 = (g .: L) as non empty Chain of Q by Th1;

          

           A4: q = ( sup M2) by Th6, A2, A3;

          for q2 st q2 in M2 holds q2 <= q1

          proof

            let q2;

            assume q2 in M2;

            then

            consider x be object such that

             A5: x in ( dom g) & x in L & q2 = (g . x) by FUNCT_1:def 6;

            reconsider x as Element of P by A5;

            set Mx = (F -image x);

            

             A6: (f . x) = ( sup Mx) by Def10;

            set y = (f . x);

            x in the carrier of P;

            then x in ( dom f) by FUNCT_2:def 1;

            then y in M1 by A5, FUNCT_1:def 6;

            then

             A7: y <= q1 by Lm18;

            q2 in (F -image x) by A5, A3;

            then q2 <= ( sup Mx) by Lm18;

            hence thesis by A7, A6, ORDERS_2: 3;

          end;

          hence thesis by A4, Lm19;

        end;

        hence thesis by A1, Lm19;

      end;

      hence thesis by Th8;

    end;

    registration

      let P, Q, F;

      cluster ( sup_func F) -> continuous;

      correctness by Lm20;

    end

    

     Lm21: ( sup_func F) is Element of ( ConPoset (P,Q))

    proof

      set x = ( sup_func F);

      

       A1: x is Element of ( Funcs (the carrier of P,the carrier of Q)) by FUNCT_2: 8;

      reconsider x = ( sup_func F) as continuous Function of P, Q;

      x in ( ConFuncs (P,Q)) by A1;

      hence thesis;

    end;

    

     Lm22: for x st x in F holds ex g be continuous Function of P, Q st x = g

    proof

      let x;

      assume x in F;

      then x in ( ConFuncs (P,Q));

      then

      consider y be Element of ( Funcs (the carrier of P,the carrier of Q)) such that

       A1: x = y & ex g be continuous Function of P, Q st g = y;

      thus thesis by A1;

    end;

    theorem :: POSET_1:11

    

     Th11: ex_sup_of (F,( ConPoset (P,Q))) & ( sup_func F) = ( "\/" (F,( ConPoset (P,Q))))

    proof

      set X = ( ConPoset (P,Q));

      set f1 = ( sup_func F);

      reconsider f = f1 as Element of ( ConPoset (P,Q)) by Lm21;

      for x be Element of X st x in F holds x <= f

      proof

        let x be Element of X;

        assume

         A1: x in F;

        then

        consider g1 be continuous Function of P, Q such that

         A2: x = g1 by Lm22;

        reconsider g = g1 as Element of X by A2;

        for p holds (g1 . p) <= (f1 . p)

        proof

          let p;

          q1 = (g1 . p) & q2 = (f1 . p) implies q1 <= q2

          proof

            assume

             A3: q1 = (g1 . p) & q2 = (f1 . p);

            then

             A4: q1 in (F -image p) by A1, A2;

            reconsider M = (F -image p) as non empty Chain of Q;

            q2 = ( sup M) by Def10, A3;

            hence thesis by A4, Lm18;

          end;

          hence thesis;

        end;

        then g1 <= f1 by YELLOW_2: 9;

        then [g, f] in ( ConRelat (P,Q)) by Def7;

        hence thesis by A2, ORDERS_2:def 5;

      end;

      then

       A5: F is_<=_than f;

      for y be Element of X holds F is_<=_than y implies f <= y

      proof

        let y be Element of X;

        y in ( ConFuncs (P,Q));

        then

        consider y1 be Element of ( Funcs (the carrier of P,the carrier of Q)) such that

         A6: y = y1 & ex gy be continuous Function of P, Q st gy = y1;

        consider gy be continuous Function of P, Q such that

         A7: gy = y1 by A6;

        F is_<=_than y implies f <= y

        proof

          assume

           A8: F is_<=_than y;

          for p holds (f1 . p) <= (gy . p)

          proof

            let p;

            q1 = (f1 . p) & q2 = (gy . p) implies q1 <= q2

            proof

              assume

               A9: q1 = (f1 . p) & q2 = (gy . p);

              reconsider M = (F -image p) as non empty Chain of Q;

              for q st q in M holds q <= q2

              proof

                let q;

                assume q in M;

                then

                consider a be Element of Q such that

                 A10: q = a & ex g be continuous Function of P, Q st g in F & a = (g . p);

                consider g be continuous Function of P, Q such that

                 A11: g in F & a = (g . p) by A10;

                reconsider g1 = g as Element of ( ConPoset (P,Q)) by A11;

                g1 <= y by A8, A11;

                then [g1, y] in ( ConRelat (P,Q)) by ORDERS_2:def 5;

                then

                consider g2,g3 be Function of P, Q such that

                 A12: g1 = g2 & y = g3 & g2 <= g3 by Def7;

                thus thesis by A12, A6, A7, A10, A11, A9, YELLOW_2: 9;

              end;

              then ( sup M) <= q2 by Lm19;

              hence thesis by A9, Def10;

            end;

            hence thesis;

          end;

          then f1 <= gy by YELLOW_2: 9;

          then [f, y] in ( ConRelat (P,Q)) by A6, A7, Def7;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis;

      end;

      hence thesis by A5, YELLOW_0: 30;

    end;

    definition

      let P, Q;

      :: POSET_1:def11

      func min_func (P,Q) -> Function of P, Q equals (P --> ( Bottom Q));

      coherence ;

    end

    registration

      let P, Q;

      cluster ( min_func (P,Q)) -> continuous;

      coherence by Th7;

    end

    

     Lm23: ( min_func (P,Q)) is Element of ( ConPoset (P,Q))

    proof

      reconsider f = ( min_func (P,Q)) as continuous Function of P, Q;

      reconsider x = f as Element of ( Funcs (the carrier of P,the carrier of Q)) by FUNCT_2: 8;

      x in ( ConFuncs (P,Q));

      hence thesis;

    end;

    theorem :: POSET_1:12

    

     Th12: for f be Element of ( ConPoset (P,Q)) st f = ( min_func (P,Q)) holds f is_<=_than the carrier of ( ConPoset (P,Q))

    proof

      let f be Element of ( ConPoset (P,Q));

      assume

       A1: f = ( min_func (P,Q));

      set f1 = ( min_func (P,Q));

      for x be Element of ( ConPoset (P,Q)) holds f <= x

      proof

        let x be Element of ( ConPoset (P,Q));

        x in ( ConFuncs (P,Q));

        then

        consider x1 be Element of ( Funcs (the carrier of P,the carrier of Q)) such that

         A2: x = x1 & ex g be continuous Function of P, Q st g = x1;

        consider g be continuous Function of P, Q such that

         A3: g = x1 by A2;

        for p holds (f1 . p) <= (g . p)

        proof

          let p;

          q1 = (f1 . p) & q2 = (g . p) implies q1 <= q2

          proof

            assume q1 = (f1 . p) & q2 = (g . p);

            then q1 = ( Bottom Q) by FUNCOP_1: 7;

            hence thesis by YELLOW_0: 44;

          end;

          hence thesis;

        end;

        then f1 <= g by YELLOW_2: 9;

        then [f, x] in ( ConRelat (P,Q)) by A2, A3, Def7, A1;

        hence thesis by ORDERS_2:def 5;

      end;

      hence thesis;

    end;

    registration

      let P, Q;

      cluster ( ConPoset (P,Q)) -> chain-complete;

      coherence

      proof

        set IT = ( ConPoset (P,Q));

        ex a be Element of IT st a is_<=_than the carrier of IT

        proof

          reconsider a = ( min_func (P,Q)) as Element of ( ConPoset (P,Q)) by Lm23;

          take a;

          thus thesis by Th12;

        end;

        then

         A1: IT is lower-bounded by YELLOW_0:def 4;

        for L be Chain of IT st L is non empty holds ex_sup_of (L,IT) by Th11;

        hence thesis by A1;

      end;

    end

    begin

    

     Lm24: x is Element of ( ConPoset (P,P)) implies x is continuous Function of P, P

    proof

      assume x is Element of ( ConPoset (P,P));

      then x in ( ConFuncs (P,P));

      then

      consider y be Element of ( Funcs (the carrier of P,the carrier of P)) such that

       A1: x = y & ex g be continuous Function of P, P st g = y;

      thus thesis by A1;

    end;

    

     Lm25: g is continuous Function of P, P implies g is Element of ( ConPoset (P,P))

    proof

      assume

       A1: g is continuous Function of P, P;

      reconsider g1 = g as Element of ( Funcs (the carrier of P,the carrier of P)) by FUNCT_2: 8;

      g1 in ( ConFuncs (P,P)) by A1;

      hence thesis;

    end;

    definition

      let P;

      :: POSET_1:def12

      func fix_func (P) -> Function of ( ConPoset (P,P)), P means

      : Def12: for g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st g = h holds (it . g) = ( least_fix_point h);

      existence

      proof

        set X = the carrier of ( ConPoset (P,P));

        set Y = the carrier of P;

        defpred U[ object, object] means for g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st g = h & g = $1 holds $2 = ( least_fix_point h);

        

         A1: for x be object st x in X holds ex y be object st y in Y & U[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider x as Element of ( ConPoset (P,P));

          reconsider h = x as continuous Function of P, P by Lm24;

          take ( least_fix_point h);

          thus thesis;

        end;

        consider IT be Function of X, Y such that

         A2: for x be object st x in X holds U[x, (IT . x)] from FUNCT_2:sch 1( A1);

        for g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st g = h holds (IT . g) = ( least_fix_point h) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be Function of ( ConPoset (P,P)), P such that

         A3: (for g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st g = h holds (h1 . g) = ( least_fix_point h)) & (for g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st g = h holds (h2 . g) = ( least_fix_point h));

        set X = the carrier of ( ConPoset (P,P));

        for x be object st x in X holds (h1 . x) = (h2 . x)

        proof

          let x be object;

          assume x in X;

          then

          reconsider g = x as Element of ( ConPoset (P,P));

          reconsider h = g as continuous Function of P, P by Lm24;

          (h1 . x) = ( least_fix_point h) by A3

          .= (h2 . x) by A3;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    

     Lm26: for p1,p2 be Element of ( ConPoset (P,P)) st p1 <= p2 holds (p1 in ( ConFuncs (P,P)) & p2 in ( ConFuncs (P,P)) & ex g1,g2 be continuous Function of P, P st p1 = g1 & p2 = g2 & g1 <= g2)

    proof

      let p1,p2 be Element of ( ConPoset (P,P));

      assume p1 <= p2;

      then

       A1: [p1, p2] in ( ConRelat (P,P)) by ORDERS_2:def 5;

      ex g1,g2 be continuous Function of P, P st p1 = g1 & p2 = g2 & g1 <= g2

      proof

        consider g1,g2 be Function of P, P such that

         A2: p1 = g1 & p2 = g2 & g1 <= g2 by A1, Def7;

        reconsider h1 = p1, h2 = p2 as continuous Function of P, P by Lm24;

        g1 = h1 by A2;

        then

        reconsider g1 as continuous Function of P, P;

        g2 = h2 by A2;

        then

        reconsider g2 as continuous Function of P, P;

        take g1, g2;

        thus thesis by A2;

      end;

      hence thesis;

    end;

    

     Lm27: ( fix_func P) is monotone Function of ( ConPoset (P,P)), P

    proof

      set IT = ( fix_func P);

      for p1,p2 be Element of ( ConPoset (P,P)) st p1 <= p2 holds for a,b be Element of P st a = (IT . p1) & b = (IT . p2) holds a <= b

      proof

        let p1,p2 be Element of ( ConPoset (P,P));

        assume

         A1: p1 <= p2;

        let a,b be Element of P;

        assume

         A2: a = (IT . p1) & b = (IT . p2);

        consider g1,g2 be continuous Function of P, P such that

         A3: p1 = g1 & p2 = g2 & g1 <= g2 by A1, Lm26;

        a = ( least_fix_point g1) & b = ( least_fix_point g2) by A2, Def12, A3;

        hence thesis by A3, Th10;

      end;

      hence thesis by ORDERS_3:def 5;

    end;

    

     Lm28: for G be non empty Chain of ( ConPoset (P,P)), n, X, x st X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } & x in X holds ex p be Element of P, g be continuous Function of P, P st x = p & g in G & p = (( iter (g,n)) . ( Bottom P))

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let n, X, x;

      assume X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } & x in X;

      then

      consider p be Element of P such that

       A1: x = p & ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P));

      thus thesis by A1;

    end;

    

     Lm29: for G be non empty Chain of ( ConPoset (P,P)), n, X st X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } holds x in X implies x is Element of P

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let n, X;

      assume

       A1: X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) };

      x in X implies x is Element of P

      proof

        assume x in X;

        then

        consider p be Element of P such that

         A2: x = p & ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) by A1;

        thus thesis by A2;

      end;

      hence thesis;

    end;

    

     Lm30: for G be non empty Chain of ( ConPoset (P,P)), n, X st X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } holds X is non empty Subset of P

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let n, X;

      assume

       A1: X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) };

      consider g be object such that

       A2: g in G by XBOOLE_0:def 1;

      reconsider g as Element of ( ConPoset (P,P)) by A2;

      reconsider gg = g as continuous Function of P, P by Lm24;

      reconsider p = (( iter (gg,n)) . ( Bottom P)) as Element of P;

      

       A3: p in X by A1, A2;

      for x be object holds x in X implies x in the carrier of P

      proof

        let x be object;

        assume x in X;

        then x is Element of the carrier of P by Lm29, A1;

        hence thesis;

      end;

      hence thesis by A3, TARSKI:def 3;

    end;

    

     Lm31: for G be non empty Chain of ( ConPoset (P,P)), f,g be monotone Function of P, P st f in G & g in G holds f <= g or g <= f

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let f,g be monotone Function of P, P;

      assume

       A1: f in G & g in G;

      set S = the InternalRel of ( ConPoset (P,P));

      

       A2: S is_strongly_connected_in G by ORDERS_2:def 7;

      per cases by A2, A1, RELAT_2:def 7;

        suppose [f, g] in S;

        then

        consider f1,g1 be Function of P, P such that

         A3: f = f1 & g = g1 & f1 <= g1 by Def7;

        thus thesis by A3;

      end;

        suppose [g, f] in S;

        then

        consider g1,f1 be Function of P, P such that

         A4: g = g1 & f = f1 & g1 <= f1 by Def7;

        thus thesis by A4;

      end;

    end;

    

     Lm32: for G be non empty Chain of ( ConPoset (P,P)), n, X st X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } holds X is non empty Chain of P

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let n, X;

      assume

       A1: X = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) };

      set R = the InternalRel of P;

      reconsider X as non empty Subset of P by A1, Lm30;

      for x,y be object holds x in X & y in X & x <> y implies [x, y] in R or [y, x] in R

      proof

        let x,y be object;

        assume

         A2: x in X & y in X & x <> y;

        then

        consider p1 be Element of P, g1 be continuous Function of P, P such that

         A3: x = p1 & g1 in G & p1 = (( iter (g1,n)) . ( Bottom P)) by A1, Lm28;

        consider p2 be Element of P, g2 be continuous Function of P, P such that

         A4: y = p2 & g2 in G & p2 = (( iter (g2,n)) . ( Bottom P)) by A1, A2, Lm28;

        per cases by A3, A4, Lm31;

          suppose g1 <= g2;

          then p1 <= p2 by Lm7, A3, A4;

          hence thesis by A3, A4, ORDERS_2:def 5;

        end;

          suppose g2 <= g1;

          then p2 <= p1 by Lm7, A3, A4;

          hence thesis by A3, A4, ORDERS_2:def 5;

        end;

      end;

      then

       A5: R is_connected_in X by RELAT_2:def 6;

      for x be object holds x in X implies [x, x] in R

      proof

        let x be object;

        assume x in X;

        then

        reconsider x as Element of P;

        x <= x;

        hence thesis by ORDERS_2:def 5;

      end;

      then R is_reflexive_in X by RELAT_2:def 1;

      then R is_strongly_connected_in X by A5, ORDERS_1: 7;

      hence thesis by ORDERS_2:def 7;

    end;

    

     Lm33: for h be Function of ( ConPoset (P,P)), P, G be non empty Chain of ( ConPoset (P,P)), x holds x in G implies (h . x) in (h .: G)

    proof

      let h be Function of ( ConPoset (P,P)), P;

      let G be non empty Chain of ( ConPoset (P,P));

      let x;

      assume

       A1: x in G;

      set X = the carrier of ( ConPoset (P,P));

      set Y = the carrier of P;

      reconsider h as Function of X, Y;

      x in X by A1;

      then x in ( dom h) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1:def 6;

    end;

    

     Lm34: for g be continuous Function of P, P, p, p1, n holds p = (( fix_func P) . g) & p1 = (( iter (g,n)) . ( Bottom P)) implies p1 <= p

    proof

      let g be continuous Function of P, P;

      let p, p1, n;

      set a = ( Bottom P);

      assume

       A1: p = (( fix_func P) . g) & p1 = (( iter (g,n)) . a);

      then

       A2: p1 in ( iterSet (g,a));

      reconsider g1 = g as Element of ( ConPoset (P,P)) by Lm25;

      reconsider G1 = g1 as continuous Function of P, P;

      p = ( least_fix_point G1) by Def12, A1

      .= ( sup ( iter_min g)) by Th9;

      hence thesis by Lm18, A2;

    end;

    

     Lm35: for G be non empty Chain of ( ConPoset (P,P)), x be set, n be Nat, M be non empty Chain of P, g1 be monotone Function of P, P st M = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } & x in (g1 .: M) holds ex g be continuous Function of P, P st g in G & x = (g1 . (( iter (g,n)) . ( Bottom P)))

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      let x be set;

      let n be Nat;

      let M be non empty Chain of P;

      let g1 be monotone Function of P, P;

      assume

       A1: M = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) } & x in (g1 .: M);

      then ex y be object st y in ( dom g1) & y in M & x = (g1 . y) by FUNCT_1:def 6;

      then

      consider y be Element of M such that

       A2: y in M & x = (g1 . y);

      consider p be Element of P such that

       A3: y = p & ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n)) . ( Bottom P)) by A1, A2;

      thus thesis by A2, A3;

    end;

    

     Lm36: for G be non empty Chain of ( ConPoset (P,P)) holds (( fix_func P) . ( sup G)) <= ( sup (( fix_func P) .: G))

    proof

      let G be non empty Chain of ( ConPoset (P,P));

      reconsider h = ( fix_func P) as monotone Function of ( ConPoset (P,P)), P by Lm27;

      (h . ( sup G)) <= ( sup (h .: G))

      proof

        reconsider L = (h .: G) as non empty Chain of P by Th1;

        set g0 = ( sup G);

        set p0 = (h . g0);

        reconsider G0 = g0 as continuous Function of P, P by Lm24;

        

         A1: p0 = ( least_fix_point G0) by Def12;

        

         A2: ( sup G) = ( sup_func G) by Th11;

        then

        reconsider g0 as continuous Function of P, P;

        set a = ( Bottom P);

        reconsider I0 = ( iterSet (g0,a)) as non empty Chain of P by Th3;

        

         A3: p0 = ( sup ( iter_min g0)) by Th9, A1

        .= ( sup I0);

        

         A4: ex_sup_of (I0,P) by Def1;

        for x be Element of P st x in I0 holds x <= ( sup L)

        proof

          let x be Element of P;

          assume x in I0;

          then

          consider y be Element of P such that

           A5: x = y & ex n be Nat st y = (( iter (g0,n)) . a);

          consider n0 be Nat such that

           A6: x = (( iter (g0,n0)) . a) by A5;

          set M0 = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,n0)) . a) };

          reconsider M0 as non empty Chain of P by Lm32;

          for p st p in M0 holds p <= ( sup L)

          proof

            let p;

            assume p in M0;

            then

            consider p0 be Element of P, g be continuous Function of P, P such that

             A7: p = p0 & g in G & p0 = (( iter (g,n0)) . a) by Lm28;

            set r = (h . g);

            r in L by A7, Lm33;

            then

            reconsider r as Element of P;

            

             A8: r <= ( sup L) by Lm18, A7, Lm33;

            p <= r by A7, Lm34;

            hence thesis by A8, ORDERS_2: 3;

          end;

          then

           A9: ( sup M0) <= ( sup L) by Lm19;

          defpred U[ Nat] means for z be Element of P, M be non empty Chain of P st z = (( iter (g0,$1)) . a) & M = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,$1)) . a) } holds z <= ( sup M);

          

           A10: U[ 0 ]

          proof

            let z be Element of P;

            let M be non empty Chain of P;

            assume z = (( iter (g0, 0 )) . a);

            then z = a by Lm1;

            hence thesis by YELLOW_0: 44;

          end;

          

           A11: U[k] implies U[(k + 1)]

          proof

            assume

             A12: U[k];

            for z1 be Element of P, M1 be non empty Chain of P st z1 = (( iter (g0,(k + 1))) . a) & M1 = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,(k + 1))) . a) } holds z1 <= ( sup M1)

            proof

              let z1 be Element of P;

              let M1 be non empty Chain of P;

              assume

               A13: z1 = (( iter (g0,(k + 1))) . a) & M1 = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,(k + 1))) . a) };

              reconsider z = (( iter (g0,k)) . a) as Element of P;

              

               A14: z1 = ((g0 * ( iter (g0,k))) . a) by A13, FUNCT_7: 71

              .= (g0 . z) by Lm2;

              reconsider M = { p where p be Element of P : ex g be Element of ( ConPoset (P,P)), h be continuous Function of P, P st h = g & g in G & p = (( iter (h,k)) . a) } as non empty Chain of P by Lm32;

              reconsider M0 = (g0 .: M) as non empty Chain of P by Th1;

              

               A15: (g0 . ( sup M)) = ( sup M0) by Th6;

              

               A16: ex_sup_of (M0,P) by Def1;

              for q be Element of P st q in M0 holds q <= ( sup M1)

              proof

                let q be Element of P;

                assume q in M0;

                then

                consider g be continuous Function of P, P such that

                 A17: g in G & q = (g0 . (( iter (g,k)) . a)) by Lm35;

                reconsider a1 = (( iter (g,k)) . a) as Element of P;

                reconsider W = (G -image a1) as non empty Chain of P;

                

                 A18: q = ( sup W) by A17, Def10, A2;

                

                 A19: ex_sup_of (W,P) by Def1;

                for q1 be Element of P st q1 in W holds q1 <= ( sup M1)

                proof

                  let q1 be Element of P;

                  assume q1 in W;

                  then

                  consider q2 be Element of P such that

                   A20: q1 = q2 & ex g1 be continuous Function of P, P st g1 in G & q2 = (g1 . a1);

                  consider g1 be continuous Function of P, P such that

                   A21: g1 in G & q1 = (g1 . a1) by A20;

                  per cases by A17, A21, Lm31;

                    suppose g1 <= g;

                    then

                     A22: q1 <= (g . a1) by A21, YELLOW_2: 9;

                    set a2 = (g . a1);

                    reconsider g2 = g as Element of ( ConPoset (P,P)) by Lm25;

                    reconsider gg = g2 as continuous Function of P, P;

                    a2 = ((g * ( iter (g,k))) . a) by Lm2

                    .= (( iter (gg,(k + 1))) . a) by FUNCT_7: 71;

                    then a2 in M1 by A13, A17;

                    then a2 <= ( sup M1) by Lm18;

                    hence thesis by A22, ORDERS_2: 3;

                  end;

                    suppose

                     A23: g <= g1;

                    reconsider a2 = (( iter (g1,k)) . a) as Element of P;

                    a1 <= a2 by A23, Lm7;

                    then

                     A24: q1 <= (g1 . a2) by A21, ORDERS_3:def 5;

                    set a3 = (g1 . a2);

                    reconsider g2 = g1 as Element of ( ConPoset (P,P)) by Lm25;

                    reconsider gg = g2 as continuous Function of P, P;

                    a3 = ((g1 * ( iter (g1,k))) . a) by Lm2

                    .= (( iter (gg,(k + 1))) . a) by FUNCT_7: 71;

                    then a3 in M1 by A13, A21;

                    then a3 <= ( sup M1) by Lm18;

                    hence thesis by A24, ORDERS_2: 3;

                  end;

                end;

                then W is_<=_than ( sup M1);

                hence thesis by A18, A19, YELLOW_0:def 9;

              end;

              then M0 is_<=_than ( sup M1);

              then

               A25: ( sup M0) <= ( sup M1) by A16, YELLOW_0:def 9;

              z <= ( sup M) by A12;

              then z1 <= ( sup M0) by A14, A15, ORDERS_3:def 5;

              hence thesis by A25, ORDERS_2: 3;

            end;

            hence thesis;

          end;

           U[k] from NAT_1:sch 2( A10, A11);

          then x <= ( sup M0) by A6;

          hence thesis by A9, ORDERS_2: 3;

        end;

        then I0 is_<=_than ( sup L);

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

      end;

      hence thesis;

    end;

    registration

      let P;

      cluster ( fix_func P) -> continuous;

      coherence

      proof

        reconsider f = ( fix_func P) as monotone Function of ( ConPoset (P,P)), P by Lm27;

        for L be non empty Chain of ( ConPoset (P,P)) holds (f . ( sup L)) <= ( sup (f .: L)) by Lm36;

        hence thesis by Th8;

      end;

    end