:: POSET_1 semantic presentation

begin

Lm1:  for f being Function st rng f c= dom f holds
iter (f,0) = id (dom f)
proof
let f be Function; ::_thesis: ( rng f c= dom f implies iter (f,0) = id (dom f) )
assume  rng f c= dom f ; ::_thesis: iter (f,0) = id (dom f)
then  field f = dom f by XBOOLE_1:12;
hence  iter (f,0) = id (dom f) by FUNCT_7:68; ::_thesis: verum
end;

Lm2:  for f being Function
for n being Nat st rng f c= dom f holds
( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f )
proof
let f be Function; ::_thesis: for n being Nat st rng f c= dom f holds
( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f )
let n be Nat; ::_thesis: ( rng f c= dom f implies ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) )
defpred S1[ Nat] means ( dom (iter (f,$1)) = dom f & rng (iter (f,$1)) c= dom f );
assume  rng f c= dom f ; ::_thesis: ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f )
then  iter (f,0) = id (dom f) by Lm1;
then A1: S1[ 0 ] by RELAT_1:45;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: ( dom (iter (f,k)) = dom f & rng (iter (f,k)) c= dom f ) ; ::_thesis: S1[k + 1]
 ( iter (f,(k + 1)) = f * (iter (f,k)) & iter (f,(k + 1)) = (iter (f,k)) * f ) by FUNCT_7:69, FUNCT_7:71;
then  ( dom (iter (f,(k + 1))) = dom (iter (f,k)) & rng (iter (f,(k + 1))) c= rng (iter (f,k)) ) by A3, RELAT_1:26, RELAT_1:27;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  ( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f ) ; ::_thesis: verum
end;

Lm3:  for X being set
for f being Function of X,X
for n being Nat holds iter (f,n) is Function of X,X
proof
let X be set ; ::_thesis: for f being Function of X,X
for n being Nat holds iter (f,n) is Function of X,X
let f be Function of X,X; ::_thesis: for n being Nat holds iter (f,n) is Function of X,X
let n be Nat; ::_thesis: iter (f,n) is Function of X,X
A1: ( X = {} implies X = {} ) ;
then A2: ( dom f = X & rng f c= X ) by FUNCT_2:def_1;
then  ( dom (iter (f,n)) = X & rng (iter (f,n)) c= X ) by Lm2;
then reconsider R = iter (f,n) as Relation of X,X by RELSET_1:4;
 ( dom R = X & rng R c= X ) by A2, Lm2;
hence  iter (f,n) is Function of X,X by A1, FUNCT_2:def_1; ::_thesis: verum
end;

registration
let P be non empty Poset;
cluster non empty strongly_connected for Element of K19( the carrier of P);
existence
 not for b1 being Chain of P holds b1 is empty
proof
 not for L being Chain of P holds L is empty
proof
set z = the Element of P;
set IT = { the Element of P};
reconsider IT = { the Element of P} as Chain of P by ORDERS_2:8;
 not IT is empty ;
hence  not for L being Chain of P holds L is empty ; ::_thesis: verum
end;
hence  not for b1 being Chain of P holds b1 is empty ; ::_thesis: verum
end;
end;

Lm4:  for A being non empty RelStr
for a being Element of A holds
( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
proof
let A be non empty RelStr ; ::_thesis: for a being Element of A holds
( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
let a be Element of A; ::_thesis: ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
 ( ( for x being Element of A holds a <= x ) implies a is_<=_than the carrier of A )
proof
assume A1: for x being Element of A holds a <= x ; ::_thesis: a is_<=_than the carrier of A
 a is_<=_than the carrier of A
proof
let x be Element of A; :: according to LATTICE3:def_8 ::_thesis: ( not x in the carrier of A or a <= x )
thus  ( not x in the carrier of A or a <= x ) by A1; ::_thesis: verum
end;
hence  a is_<=_than the carrier of A ; ::_thesis: verum
end;
hence  ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) by LATTICE3:def_8; ::_thesis: verum
end;

definition
let IT be RelStr ;
attrIT is chain-complete  means :Def1: :: POSET_1:def 1
( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) );
end;

:: deftheorem Def1 defines chain-complete POSET_1:def_1_:_
 for IT being RelStr holds
( IT is chain-complete iff ( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) ) );

theorem Th1: :: POSET_1:1
for P1, P2 being non empty Poset
for K being non empty Chain of P1
for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2
proof
let P1, P2 be non empty Poset; ::_thesis: for K being non empty Chain of P1
for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2
let K be non empty Chain of P1; ::_thesis: for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2
let h be monotone Function of P1,P2; ::_thesis: h .: K is non empty Chain of P2
set R = the InternalRel of P2;
set K2 = h .: K;
 for x, y being set st x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 holds
[y,x] in the InternalRel of P2
proof
let x, y be set ; ::_thesis: ( x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 implies [y,x] in the InternalRel of P2 )
assume A1: ( x in h .: K & y in h .: K & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 )
then reconsider x = x, y = y as Element of P2 ;
consider a being set  such that
A2: ( a in dom h & a in K & x = h . a ) by A1, FUNCT_1:def_6;
consider b being set  such that
A3: ( b in dom h & b in K & y = h . b ) by A1, FUNCT_1:def_6;
reconsider a = a, b = 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  ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 ) by ORDERS_2:def_5; ::_thesis: verum
end;
then A4: the InternalRel of P2 is_connected_in h .: K by RELAT_2:def_6;
 for x being set st x in h .: K holds
[x,x] in the InternalRel of P2
proof
let x be set ; ::_thesis: ( x in h .: K implies [x,x] in the InternalRel of P2 )
assume  x in h .: K ; ::_thesis: [x,x] in the InternalRel of P2
then reconsider x = x as Element of P2 ;
 x <= x ;
hence  [x,x] in the InternalRel of P2 by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of P2 is_reflexive_in h .: K by RELAT_2:def_1;
then  the InternalRel of P2 is_strongly_connected_in h .: K by A4, ORDERS_1:7;
then reconsider K2 = h .: K as Chain of P2 by ORDERS_2:def_7;
consider a being set  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  h .: K is non empty Chain of P2 ; ::_thesis: verum
end;

registration
cluster non empty strict V55() reflexive transitive antisymmetric chain-complete for RelStr ;
existence
 ex b1 being Poset st
( b1 is strict & b1 is chain-complete & not b1 is empty )
proof
set z = the set ;
set A = { the set };
reconsider R = id { the set } as Relation of { the set } ;
reconsider R = R as Order of { the set } ;
take IT = RelStr(# { the set },R #); ::_thesis: ( IT is strict & IT is chain-complete & not IT is empty )
reconsider z = the set as Element of IT by TARSKI:def_1;
 for L being Chain of IT st not L is empty holds
ex_sup_of L,IT
proof
let L be Chain of IT; ::_thesis: ( not L is empty implies ex_sup_of L,IT )
assume  not L is empty ; ::_thesis: ex_sup_of L,IT
 for x being Element of IT st x in L holds
x <= z by TARSKI:def_1;
then A1: L is_<=_than z by LATTICE3:def_9;
 for y being Element of IT st L is_<=_than y holds
z <= y by TARSKI:def_1;
hence  ex_sup_of L,IT by A1, YELLOW_0:15; ::_thesis: verum
end;
hence  ( IT is strict & IT is chain-complete & not IT is empty ) by Def1; ::_thesis: verum
end;
end;

registration
cluster chain-complete  ->  lower-bounded for RelStr ;
coherence
 for b1 being RelStr st b1 is chain-complete holds
b1 is lower-bounded by Def1;
end;


theorem Th2: :: POSET_1:2
for P, Q being non empty strict chain-complete Poset
for L being non empty Chain of P
for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for L being non empty Chain of P
for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)
let L be non empty Chain of P; ::_thesis: for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)
let f be monotone Function of P,Q; ::_thesis: sup (f .: L) <= f . (sup L)
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 being Element of Q st q in M holds
q <= f . (sup L)
proof
let q be Element of Q; ::_thesis: ( q in M implies q <= f . (sup L) )
assume  q in M ; ::_thesis: q <= f . (sup L)
then consider x being set  such that
A2: ( x in dom f & x in L & q = f . x ) by FUNCT_1:def_6;
reconsider x = x as Element of P by A2;
 L is_<=_than sup L by A1, YELLOW_0:def_9;
then  x <= sup L by A2, LATTICE3:def_9;
hence  q <= f . (sup L) by A2, ORDERS_3:def_5; ::_thesis: verum
end;
then  M is_<=_than f . (sup L) by LATTICE3:def_9;
hence  sup (f .: L) <= f . (sup L) by A1, YELLOW_0:def_9; ::_thesis: verum
end;

begin

Lm5:  for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds (iter (g,0)) . p = p
proof
let P be non empty Poset; ::_thesis: for g being monotone Function of P,P
for p being Element of P holds (iter (g,0)) . p = p
let g be monotone Function of P,P; ::_thesis: for p being Element of P holds (iter (g,0)) . p = p
let p be Element of P; ::_thesis: (iter (g,0)) . p = p
set X = the carrier of P;
(iter (g,0)) . p = (id the carrier of P) . p by FUNCT_7:84
.= p by FUNCT_1:18 ;
hence  (iter (g,0)) . p = p ; ::_thesis: verum
end;

definition
let P be non empty Poset;
let g be monotone Function of P,P;
let p be Element of P;
func iterSet (g,p) ->  non empty set  equals :: POSET_1:def 2
 {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  ;
correctness
coherence
{  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  is non empty set ;
proof
set IT =  {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  ;
 not  {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  is empty
proof
 (iter (g,0)) . p = p by Lm5;
then  p in  {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  ;
hence  not  {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  is empty ; ::_thesis: verum
end;
hence   {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  is non empty set ; ::_thesis: verum
end;
end;

:: deftheorem  defines iterSet POSET_1:def_2_:_
 for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds iterSet (g,p) =  {  x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p  }  ;

Lm6:  for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P
proof
let n be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P
let P be non empty strict chain-complete Poset; ::_thesis: for p being Element of P
for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P
let p be Element of P; ::_thesis: for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P
let g be monotone Function of P,P; ::_thesis: (iter (g,n)) . p is Element of P
set X = the carrier of P;
reconsider g1 = iter (g,n) as Function of the carrier of P, the carrier of P by Lm3;
 g1 . p in the carrier of P ;
hence  (iter (g,n)) . p is Element of P ; ::_thesis: verum
end;

Lm7:  for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
proof
let n be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
let P be non empty strict chain-complete Poset; ::_thesis: for p being Element of P
for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
let p be Element of P; ::_thesis: for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
let g be monotone Function of P,P; ::_thesis: ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
set X = the carrier of P;
reconsider g1 = iter (g,n) as Function of the carrier of P, the carrier of P by Lm3;
 ( (g * g1) . p = g . (g1 . p) & (g1 * g) . p = g1 . (g . p) ) by FUNCT_2:15;
hence  ( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) ) ; ::_thesis: verum
end;

Lm8:  for n being Nat
for P being non empty strict chain-complete Poset
for p, p3, p1, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
proof
let n be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p, p3, p1, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let P be non empty strict chain-complete Poset; ::_thesis: for p, p3, p1, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let p, p3, p1, p4 be Element of P; ::_thesis: for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
let g be monotone Function of P,P; ::_thesis: ( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 )
defpred S1[ Nat] means  for p, p3, p1, p4 being Element of P st p <= p3 & p1 = (iter (g,$1)) . p & p4 = (iter (g,$1)) . p3 holds
p1 <= p4;
A1: S1[ 0 ]
proof
let p, p3, p1, p4 be Element of P; ::_thesis: ( p <= p3 & p1 = (iter (g,0)) . p & p4 = (iter (g,0)) . p3 implies p1 <= p4 )
assume  ( p <= p3 & p1 = (iter (g,0)) . p & p4 = (iter (g,0)) . p3 ) ; ::_thesis: p1 <= p4
then  ( p <= p3 & p1 = p & p4 = p3 ) by Lm5;
hence  p1 <= p4 ; ::_thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for p, p3, p1, p4 being Element of P st p <= p3 & p1 = (iter (g,k)) . p & p4 = (iter (g,k)) . p3 holds
p1 <= p4 ; ::_thesis: S1[k + 1]
 S1[k + 1]
proof
let p, p3, p1, p4 be Element of P; ::_thesis: ( p <= p3 & p1 = (iter (g,(k + 1))) . p & p4 = (iter (g,(k + 1))) . p3 implies p1 <= p4 )
assume A4: ( p <= p3 & p1 = (iter (g,(k + 1))) . p & p4 = (iter (g,(k + 1))) . p3 ) ; ::_thesis: p1 <= p4
reconsider x1 = (iter (g,k)) . p as Element of P by Lm6;
reconsider y1 = (iter (g,k)) . p3 as Element of P by Lm6;
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 Lm7, A4;
hence  p1 <= p4 by A5, ORDERS_3:def_5; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  ( p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 implies p1 <= p4 ) ; ::_thesis: verum
end;

Lm9:  for n, k being Nat
for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
proof
let n, k be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let P be non empty strict chain-complete Poset; ::_thesis: for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let p3, p, p1, p4 be Element of P; ::_thesis: for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
let g be monotone Function of P,P; ::_thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 )
defpred S1[ Nat] means  for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + $1))) . p holds
p1 <= p4;
A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for p, p3, p1, p4 being Element of P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4 ; ::_thesis: S1[k + 1]
 S1[k + 1]
proof
let p, p3, p1, p4 be Element of P; ::_thesis: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p implies p1 <= p4 )
assume A4: ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + (k + 1)))) . p ) ; ::_thesis: p1 <= p4
reconsider y1 = (iter (g,(n + k))) . p as Element of P by Lm6;
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 Lm7, A4;
then  y1 <= p4 by A4, Lm8;
hence  p1 <= p4 by A5, ORDERS_2:3; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  ( p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p implies p1 <= p4 ) ; ::_thesis: verum
end;

Lm10:  for n, m being Nat
for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
proof
let n, m be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let P be non empty strict chain-complete Poset; ::_thesis: for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let p3, p, p1, p4 be Element of P; ::_thesis: for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
let g be monotone Function of P,P; ::_thesis: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p implies p1 <= p4 )
assume A1: ( n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p ) ; ::_thesis: p1 <= p4
then consider k being Nat such that
A2: m = n + k by NAT_1:10;
thus  p1 <= p4 by A1, A2, Lm9; ::_thesis: verum
end;

Lm11:  for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
proof
let n be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
let P be non empty strict chain-complete Poset; ::_thesis: for p being Element of P
for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
let p be Element of P; ::_thesis: for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
let g be monotone Function of P,P; ::_thesis: ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p )
defpred S1[ Nat] means  for p being Element of P st p is_a_fixpoint_of g holds
(iter (g,$1)) . p = p;
A1: S1[ 0 ] by Lm5;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 S1[k + 1]
proof
let p be Element of P; ::_thesis: ( p is_a_fixpoint_of g implies (iter (g,(k + 1))) . p = p )
assume A4: p is_a_fixpoint_of g ; ::_thesis: (iter (g,(k + 1))) . p = p
 iter (g,(k + 1)) = g * (iter (g,k)) by FUNCT_7:71;
then (iter (g,(k + 1))) . p = g . ((iter (g,k)) . p) by Lm7
.= g . p by A4, A3
.= p by A4, ABIAN:def_3 ;
hence  (iter (g,(k + 1))) . p = p ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  ( p is_a_fixpoint_of g implies (iter (g,n)) . p = p ) ; ::_thesis: verum
end;

Lm12:  for n being Nat
for P being non empty strict chain-complete Poset
for p1, p, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
proof
let n be Nat; ::_thesis: for P being non empty strict chain-complete Poset
for p1, p, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let P be non empty strict chain-complete Poset; ::_thesis: for p1, p, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let p1, p, p2 be Element of P; ::_thesis: for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
let g1, g2 be monotone Function of P,P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 )
defpred S1[ Nat] means  for p, p1, p2 being Element of P st g1 <= g2 & p1 = (iter (g1,$1)) . p & p2 = (iter (g2,$1)) . p holds
p1 <= p2;
A1: S1[ 0 ]
proof
let p, p1, p2 be Element of P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,0)) . p & p2 = (iter (g2,0)) . p implies p1 <= p2 )
assume  ( g1 <= g2 & p1 = (iter (g1,0)) . p & p2 = (iter (g2,0)) . p ) ; ::_thesis: p1 <= p2
then  ( p1 = p & p2 = p ) by Lm5;
hence  p1 <= p2 ; ::_thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 S1[k + 1]
proof
let p, p1, p2 be Element of P; ::_thesis: ( g1 <= g2 & p1 = (iter (g1,(k + 1))) . p & p2 = (iter (g2,(k + 1))) . p implies p1 <= p2 )
assume A4: ( g1 <= g2 & p1 = (iter (g1,(k + 1))) . p & p2 = (iter (g2,(k + 1))) . p ) ; ::_thesis: p1 <= p2
reconsider q1 = (iter (g1,k)) . p as Element of P by Lm6;
reconsider q2 = (iter (g2,k)) . p as Element of P by Lm6;
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 Lm7, A4;
 iter (g2,(k + 1)) = g2 * (iter (g2,k)) by FUNCT_7:71;
then A7: p2 = g2 . q2 by Lm7, A4;
A8: p1 <= g1 . q2 by A5, A6, ORDERS_3:def_5;
 g1 . q2 <= p2 by A4, A7, YELLOW_2:9;
hence  p1 <= p2 by A8, ORDERS_2:3; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  ( g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p implies p1 <= p2 ) ; ::_thesis: verum
end;

theorem Th3: :: POSET_1:3
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P
let g be monotone Function of P,P; ::_thesis: iterSet (g,(Bottom P)) is non empty Chain of P
set a = Bottom P;
set R = the InternalRel of P;
set L = iterSet (g,(Bottom P));
A1: for x being set st x in iterSet (g,(Bottom P)) holds
x is Element of P
proof
let x be set ; ::_thesis: ( x in iterSet (g,(Bottom P)) implies x is Element of P )
assume  x in iterSet (g,(Bottom P)) ; ::_thesis: x is Element of P
then consider y being Element of P such that
A2: ( x = y & ex n being Nat st y = (iter (g,n)) . (Bottom P) ) ;
thus  x is Element of P by A2; ::_thesis: verum
end;
 for x being set st x in iterSet (g,(Bottom P)) holds
x in the carrier of P
proof
let x be set ; ::_thesis: ( x in iterSet (g,(Bottom P)) implies x in the carrier of P )
assume  x in iterSet (g,(Bottom P)) ; ::_thesis: x in the carrier of P
then  x is Element of the carrier of P by A1;
hence  x in the carrier of P ; ::_thesis: verum
end;
then reconsider L = iterSet (g,(Bottom P)) as Subset of P by TARSKI:def_3;
 for x, y being set st x in L & y in L & x <> y & not [x,y] in the InternalRel of P holds
[y,x] in the InternalRel of P
proof
let x, y be set ; ::_thesis: ( x in L & y in L & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P )
assume A3: ( x in L & y in L & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then reconsider x = x, y = y as Element of P ;
consider p being Element of P such that
A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) by A3;
consider p1 being Element of P such that
A5: ( y = p1 & ex m being Nat st p1 = (iter (g,m)) . (Bottom P) ) by A3;
consider n being Nat such that
A6: p = (iter (g,n)) . (Bottom P) by A4;
consider m being Nat such that
A7: p1 = (iter (g,m)) . (Bottom P) by A5;
 ( p <= p1 or p1 <= p )
proof
set a1 = (iter (g,1)) . (Bottom P);
A8: (iter (g,1)) . (Bottom P) = g . (Bottom P) by FUNCT_7:70;
percases ( n <= m or m <= n ) ;
suppose n <= m ; ::_thesis: ( p <= p1 or p1 <= p )
hence  ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm10, YELLOW_0:44; ::_thesis: verum
end;
suppose m <= n ; ::_thesis: ( p <= p1 or p1 <= p )
hence  ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm10, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4, A5, ORDERS_2:def_5; ::_thesis: verum
end;
then A9: the InternalRel of P is_connected_in L by RELAT_2:def_6;
 for x being set st x in L holds
[x,x] in the InternalRel of P
proof
let x be set ; ::_thesis: ( x in L implies [x,x] in the InternalRel of P )
assume  x in L ; ::_thesis: [x,x] in the InternalRel of P
then reconsider x = x as Element of P ;
 x <= x ;
hence  [x,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of P is_reflexive_in L by RELAT_2:def_1;
then  the InternalRel of P is_strongly_connected_in L by A9, ORDERS_1:7;
then reconsider L = L as Chain of P by ORDERS_2:def_7;
 L is non empty Chain of P ;
hence  iterSet (g,(Bottom P)) is non empty Chain of P ; ::_thesis: verum
end;

definition
let P be non empty strict chain-complete Poset;
let g be monotone Function of P,P;
func iter_min g ->  non empty Chain of P equals :: POSET_1:def 3
 iterSet (g,(Bottom P));
correctness
coherence
iterSet (g,(Bottom P)) is non empty Chain of P;
by Th3;
end;

:: deftheorem  defines iter_min POSET_1:def_3_:_
 for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iter_min g = iterSet (g,(Bottom P));

theorem Th4: :: POSET_1:4
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))
let g be monotone Function of P,P; ::_thesis: sup (iter_min g) = sup (g .: (iter_min g))
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 sup (iter_min g) by A1, YELLOW_0:def_9;
A3: L is_<=_than sup L by A1, YELLOW_0:def_9;
 for x being Element of P st x in iter_min g holds
x <= sup L
proof
let x be Element of P; ::_thesis: ( x in iter_min g implies x <= sup L )
assume  x in iter_min g ; ::_thesis: x <= sup L
then consider p being Element of P such that
A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p = (iter (g,n)) . (Bottom P) by A4;
A6: ( 1 <= n implies p in L )
proof
assume  1 <= n ; ::_thesis: p in L
then consider k being Nat such that
A7: n = 1 + k by NAT_1:10;
reconsider z = (iter (g,k)) . (Bottom P) as Element of P by Lm6;
 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))) . (Bottom P) by A5, A7, FUNCT_7:71
.= g . z by Lm7 ;
hence  p in L by A8, FUNCT_1:def_6; ::_thesis: verum
end;
 ( n = 0 implies p = Bottom P ) by A5, Lm5;
hence  x <= sup L by A6, A4, A3, LATTICE3:def_9, NAT_1:14, YELLOW_0:44; ::_thesis: verum
end;
then  iter_min g is_<=_than sup L by LATTICE3:def_9;
then A9: sup (iter_min g) <= sup L by A1, YELLOW_0:30;
 for x being Element of P st x in L holds
x <= sup (iter_min g)
proof
let x be Element of P; ::_thesis: ( x in L implies x <= sup (iter_min g) )
assume  x in L ; ::_thesis: x <= sup (iter_min g)
then consider z being set  such that
A10: ( z in dom g & z in iter_min g & x = g . z ) by FUNCT_1:def_6;
consider z1 being Element of P such that
A11: ( z = z1 & ex n being Nat st z1 = (iter (g,n)) . (Bottom P) ) by A10;
consider n being Nat such that
A12: z1 = (iter (g,n)) . (Bottom P) by A11;
set n1 = n + 1;
g . z = (g * (iter (g,n))) . (Bottom P) by Lm7, A11, A12
.= (iter (g,(n + 1))) . (Bottom P) by FUNCT_7:71 ;
then  x in iterSet (g,(Bottom P)) by A10;
hence  x <= sup (iter_min g) by A2, LATTICE3:def_9; ::_thesis: verum
end;
then  L is_<=_than sup (iter_min g) by LATTICE3:def_9;
then  sup L <= sup (iter_min g) by A1, YELLOW_0:def_9;
hence  sup (iter_min g) = sup (g .: (iter_min g)) by A9, ORDERS_2:2; ::_thesis: verum
end;

theorem Th5: :: POSET_1:5
for P being non empty strict chain-complete Poset
for g1, g2 being monotone Function of P,P st g1 <= g2 holds
sup (iter_min g1) <= sup (iter_min g2)
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g1, g2 being monotone Function of P,P st g1 <= g2 holds
sup (iter_min g1) <= sup (iter_min g2)
let g1, g2 be monotone Function of P,P; ::_thesis: ( g1 <= g2 implies sup (iter_min g1) <= sup (iter_min g2) )
assume A1: g1 <= g2 ; ::_thesis: sup (iter_min g1) <= sup (iter_min 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 sup (iter_min g2) by YELLOW_0:def_9;
 for x being Element of P st x in iter_min g1 holds
x <= sup (iter_min g2)
proof
let x be Element of P; ::_thesis: ( x in iter_min g1 implies x <= sup (iter_min g2) )
assume  x in iter_min g1 ; ::_thesis: x <= sup (iter_min g2)
then consider p being Element of P such that
A4: ( x = p & ex n being Nat st p = (iter (g1,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p = (iter (g1,n)) . (Bottom P) by A4;
reconsider y = (iter (g2,n)) . (Bottom P) as Element of P by Lm6;
 y in iter_min g2 ;
then A6: y <= sup (iter_min g2) by A3, LATTICE3:def_9;
 p <= y by A1, A5, Lm12;
hence  x <= sup (iter_min g2) by A4, A6, ORDERS_2:3; ::_thesis: verum
end;
then  iter_min g1 is_<=_than sup (iter_min g2) by LATTICE3:def_9;
hence  sup (iter_min g1) <= sup (iter_min g2) by A2, YELLOW_0:30; ::_thesis: verum
end;

definition
let P, Q be non empty Poset;
let f be Function of P,Q;
attrf is continuous  means :Def4: :: POSET_1:def 4
( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) );
end;

:: deftheorem Def4 defines continuous POSET_1:def_4_:_
 for P, Q being non empty Poset
for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) ) );

theorem Th6: :: POSET_1:6
for P, Q being non empty strict chain-complete Poset
for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )
let f be Function of P,Q; ::_thesis: ( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )
thus  ( f is continuous implies ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) ) ::_thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) implies f is continuous )
proof
assume A1: f is continuous ; ::_thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) )
 for L being non empty Chain of P holds f . (sup L) = sup (f .: L)
proof
let L be non empty Chain of P; ::_thesis: f . (sup L) = sup (f .: L)
A2: f preserves_sup_of L by A1, Def4;
 ex_sup_of L,P by Def1;
hence  f . (sup L) = sup (f .: L) by A2, WAYBEL_0:def_31; ::_thesis: verum
end;
hence  ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) by A1, Def4; ::_thesis: verum
end;
assume that
A3: f is monotone and
A4: for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ; ::_thesis: f is continuous
 for L being non empty Chain of P holds f preserves_sup_of L
proof
let L be non empty Chain of P; ::_thesis: f preserves_sup_of 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  f preserves_sup_of L by WAYBEL_0:def_31; ::_thesis: verum
end;
hence  f is continuous by A3, Def4; ::_thesis: verum
end;

theorem Th7: :: POSET_1:7
for Q, P being non empty strict chain-complete Poset
for z being Element of Q holds P --> z is continuous
proof
let Q, P be non empty strict chain-complete Poset; ::_thesis: for z being Element of Q holds P --> z is continuous
let z be Element of Q; ::_thesis: P --> z is continuous
set IT = P --> z;
 for L being non empty Chain of P holds (P --> z) . (sup L) = sup ((P --> z) .: L)
proof
let L be non empty Chain of P; ::_thesis: (P --> z) . (sup L) = sup ((P --> z) .: L)
set M = (P --> z) .: L;
 for x being Element of Q st x in (P --> z) .: L holds
x <= z
proof
let x be Element of Q; ::_thesis: ( x in (P --> z) .: L implies x <= z )
assume  x in (P --> z) .: L ; ::_thesis: x <= z
then consider a being set  such that
A1: ( a in dom (P --> z) & a in L & x = (P --> z) . a ) by FUNCT_1:def_6;
thus  x <= z by A1, FUNCOP_1:7; ::_thesis: verum
end;
then A2: (P --> z) .: L is_<=_than z by LATTICE3:def_9;
 for y being Element of Q st (P --> z) .: L is_<=_than y holds
z <= y
proof
let y be Element of Q; ::_thesis: ( (P --> z) .: L is_<=_than y implies z <= y )
assume A3: (P --> z) .: L is_<=_than y ; ::_thesis: z <= y
consider a being set  such that
A4: a in L by XBOOLE_0:def_1;
 a in the carrier of P by A4;
then A5: a in dom (P --> z) by FUNCOP_1:13;
 (P --> z) . a = z by A4, FUNCOP_1:7;
then  z in (P --> z) .: L by A4, A5, FUNCT_1:def_6;
hence  z <= y by A3, LATTICE3:def_9; ::_thesis: verum
end;
then  z = "\/" (((P --> z) .: L),Q) by A2, YELLOW_0:30;
hence  (P --> z) . (sup L) = sup ((P --> z) .: L) by FUNCOP_1:7; ::_thesis: verum
end;
hence  P --> z is continuous by Th6; ::_thesis: verum
end;

registration
let P, Q be non empty strict chain-complete Poset;
cluster Relation-like the carrier of P -defined the carrier of Q -valued Function-like quasi_total continuous for Element of K19(K20( the carrier of P, the carrier of Q));
existence
 ex b1 being Function of P,Q st b1 is continuous
proof
set z = the Element of Q;
take  P --> the Element of Q ; ::_thesis: P --> the Element of Q is continuous
thus  P --> the Element of Q is continuous by Th7; ::_thesis: verum
end;
end;

registration
let P, Q be non empty strict chain-complete Poset;
cluster Function-like quasi_total continuous  ->  monotone for Element of K19(K20( the carrier of P, the carrier of Q));
correctness
coherence
for b1 being Function of P,Q st b1 is continuous holds
b1 is monotone ;
by Def4;
end;

theorem Th8: :: POSET_1:8
for P, Q being non empty strict chain-complete Poset
for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds
f is continuous
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds
f is continuous
let f be monotone Function of P,Q; ::_thesis: ( ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) implies f is continuous )
assume A1: for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ; ::_thesis: f is continuous
 for L being non empty Chain of P holds f . (sup L) = sup (f .: L)
proof
let L be non empty Chain of P; ::_thesis: f . (sup L) = sup (f .: L)
set a1 = f . (sup L);
set a2 = sup (f .: L);
A2: sup (f .: L) <= f . (sup L) by Th2;
 f . (sup L) <= sup (f .: L) by A1;
hence  f . (sup L) = sup (f .: L) by A2, ORDERS_2:2; ::_thesis: verum
end;
hence  f is continuous by Th6; ::_thesis: verum
end;

Lm13:  for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
proof
let P be non empty strict chain-complete Poset; ::_thesis: for p being Element of P
for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
let p be Element of P; ::_thesis: for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
let g be monotone Function of P,P; ::_thesis: ( g is continuous & p = sup (iter_min g) implies p is_a_fixpoint_of g )
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) ) ; ::_thesis: p is_a_fixpoint_of g
then g . p = sup L by Th6
.= p by A2, Th4 ;
hence  p is_a_fixpoint_of g by A1, ABIAN:def_3; ::_thesis: verum
end;

Lm14:  for P being non empty strict chain-complete Poset
for p4 being Element of P
for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
proof
let P be non empty strict chain-complete Poset; ::_thesis: for p4 being Element of P
for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
let p4 be Element of P; ::_thesis: for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
let g be monotone Function of P,P; ::_thesis: ( p4 = sup (iter_min g) implies for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p )
assume A1: p4 = sup (iter_min g) ; ::_thesis: for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
 for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
proof
let p be Element of P; ::_thesis: ( p is_a_fixpoint_of g implies p4 <= p )
assume A2: p is_a_fixpoint_of g ; ::_thesis: p4 <= p
set M = iter_min g;
set a = Bottom P;
A3: ex_sup_of iter_min g,P by Def1;
 for p1 being Element of P st p1 in iter_min g holds
p1 <= p
proof
let p1 be Element of P; ::_thesis: ( p1 in iter_min g implies p1 <= p )
assume  p1 in iter_min g ; ::_thesis: p1 <= p
then consider p2 being Element of P such that
A4: ( p1 = p2 & ex n being Nat st p2 = (iter (g,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p1 = (iter (g,n)) . (Bottom P) by A4;
reconsider q = (iter (g,n)) . p as Element of P by Lm6;
 p1 <= q by A5, Lm8, YELLOW_0:44;
hence  p1 <= p by A2, Lm11; ::_thesis: verum
end;
then  iter_min g is_<=_than p by LATTICE3:def_9;
hence  p4 <= p by A3, A1, YELLOW_0:def_9; ::_thesis: verum
end;
hence  for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p ; ::_thesis: verum
end;

definition
let P be non empty strict chain-complete Poset;
let g be monotone Function of P,P;
assume A1: g is continuous ;
func least_fix_point g ->  Element of P means :Def5: :: POSET_1:def 5
( it is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
it <= p ) );
existence
 ex b1 being Element of P st
( b1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b1 <= p ) )
proof
set IT = sup (iter_min g);
take  sup (iter_min g) ; ::_thesis: ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
sup (iter_min g) <= p ) )
thus  ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
sup (iter_min g) <= p ) ) by A1, Lm13, Lm14; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of P st b1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b1 <= p ) & b2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b2 <= p ) holds
b1 = b2
proof
let p1, p2 be Element of P; ::_thesis: ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p2 <= p ) implies p1 = p2 )
assume  ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p2 <= p ) ) ; ::_thesis: p1 = p2
then  ( p1 <= p2 & p2 <= p1 ) ;
hence  p1 = p2 by ORDERS_2:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines least_fix_point POSET_1:def_5_:_
 for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous holds
for b3 being Element of P holds
( b3 = least_fix_point g iff ( b3 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b3 <= p ) ) );

theorem Th9: :: POSET_1:9
for P being non empty strict chain-complete Poset
for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)
let g be continuous Function of P,P; ::_thesis: least_fix_point g = sup (iter_min g)
set p = sup (iter_min g);
set q = least_fix_point g;
 sup (iter_min g) is_a_fixpoint_of g by Lm13;
then A1: least_fix_point g <= sup (iter_min g) by Def5;
 least_fix_point g is_a_fixpoint_of g by Def5;
then  sup (iter_min g) <= least_fix_point g by Lm14;
hence  least_fix_point g = sup (iter_min g) by A1, ORDERS_2:2; ::_thesis: verum
end;

theorem Th10: :: POSET_1:10
for P being non empty strict chain-complete Poset
for g1, g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point g1 <= least_fix_point g2
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g1, g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point g1 <= least_fix_point g2
let g1, g2 be continuous Function of P,P; ::_thesis: ( g1 <= g2 implies least_fix_point g1 <= least_fix_point g2 )
assume A1: g1 <= g2 ; ::_thesis: least_fix_point g1 <= least_fix_point g2
set p1 = sup (iter_min g1);
set p2 = sup (iter_min g2);
 ( sup (iter_min g1) = least_fix_point g1 & sup (iter_min g2) = least_fix_point g2 ) by Th9;
hence  least_fix_point g1 <= least_fix_point g2 by A1, Th5; ::_thesis: verum
end;

begin

definition
let P, Q be non empty strict chain-complete Poset;
func ConFuncs (P,Q) ->  non empty set  equals :: POSET_1:def 6
 {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  ;
correctness
coherence
{  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  is non empty set ;
proof
set IT =  {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  ;
 not  {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  is empty
proof
set z = the Element of Q;
reconsider f = P --> the Element of Q 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  {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  ;
hence  not  {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  is empty ; ::_thesis: verum
end;
hence   {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  is non empty set ; ::_thesis: verum
end;
end;

:: deftheorem  defines ConFuncs POSET_1:def_6_:_
 for P, Q being non empty strict chain-complete Poset holds ConFuncs (P,Q) =  {  x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x  }  ;

Lm15:  for P, Q being non empty strict chain-complete Poset
for f being Function of P,Q holds f <= f
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being Function of P,Q holds f <= f
let f be Function of P,Q; ::_thesis: f <= f
 for p being Element of P holds f . p <= f . p ;
hence  f <= f by YELLOW_2:9; ::_thesis: verum
end;

Lm16:  for P, Q being non empty strict chain-complete Poset
for f, g, h being Function of P,Q st f <= g & g <= h holds
f <= h
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f, g, h being Function of P,Q st f <= g & g <= h holds
f <= h
let f, g, h be Function of P,Q; ::_thesis: ( f <= g & g <= h implies f <= h )
assume A1: ( f <= g & g <= h ) ; ::_thesis: f <= h
 for p being Element of P holds f . p <= h . p
proof
let p be Element of P; ::_thesis: f . p <= h . p
 for q, q2 being Element of Q st q = f . p & q2 = h . p holds
q <= q2
proof
let q, q2 be Element of Q; ::_thesis: ( q = f . p & q2 = h . p implies q <= q2 )
assume A2: ( q = f . p & q2 = h . p ) ; ::_thesis: q <= q2
set q1 = g . p;
 ( q <= g . p & g . p <= q2 ) by A2, A1, YELLOW_2:9;
hence  q <= q2 by ORDERS_2:3; ::_thesis: verum
end;
hence  f . p <= h . p ; ::_thesis: verum
end;
hence  f <= h by YELLOW_2:9; ::_thesis: verum
end;

Lm17:  for P, Q being non empty strict chain-complete Poset
for f, g being Function of P,Q st f <= g & g <= f holds
f = g
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f, g being Function of P,Q st f <= g & g <= f holds
f = g
let f, g be Function of P,Q; ::_thesis: ( f <= g & g <= f implies f = g )
assume A1: ( f <= g & g <= f ) ; ::_thesis: f = g
 for x being set st x in the carrier of P holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in the carrier of P implies f . x = g . x )
assume  x in the carrier of P ; ::_thesis: f . x = g . x
then reconsider p = x as Element of P ;
set q1 = f . p;
set q2 = g . p;
A2: f . p <= g . p by A1, YELLOW_2:9;
 g . p <= f . p by A1, YELLOW_2:9;
hence  f . x = g . x by A2, ORDERS_2:2; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;

definition
let P, Q be non empty strict chain-complete Poset;
func ConRelat (P,Q) ->  Relation of (ConFuncs (P,Q)) means :Def7: :: POSET_1:def 7
 for x, y being set holds
( [x,y] in it iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) );
existence
 ex b1 being Relation of (ConFuncs (P,Q)) st
for x, y being set holds
( [x,y] in b1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) )
proof
defpred S1[ set , set ] means  ex f, g being Function of P,Q st
( $1 = f & $2 = g & f <= g );
set X = ConFuncs (P,Q);
consider IT being Relation of (ConFuncs (P,Q)),(ConFuncs (P,Q)) such that
A1: for x, y being set holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & S1[x,y] ) ) from RELSET_1:sch_1();
take  IT ; ::_thesis: for x, y being set holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) )
thus  for x, y being set holds
( [x,y] in IT iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of (ConFuncs (P,Q)) st ( for x, y being set holds
( [x,y] in b1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) holds
b1 = b2
proof
set X = ConFuncs (P,Q);
let Y1, Y2 be Relation of (ConFuncs (P,Q)); ::_thesis: ( ( for x, y being set holds
( [x,y] in Y1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds
( [x,y] in Y2 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) implies Y1 = Y2 )
defpred S1[ set , set ] means ( $1 in ConFuncs (P,Q) & $2 in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( $1 = f & $2 = g & f <= g ) );
 ( ( for x, y being set holds
( ( [x,y] in Y1 implies S1[x,y] ) & ( S1[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds
( [x,y] in Y2 iff S1[x,y] ) ) ) ) implies Y1 = Y2 )
proof
assume A2: for x, y being set holds
( ( [x,y] in Y1 implies S1[x,y] ) & ( S1[x,y] implies [x,y] in Y1 ) & ( for x, y being set holds
( [x,y] in Y2 iff S1[x,y] ) ) ) ; ::_thesis: Y1 = Y2
then A3: for x1, y1 being Element of ConFuncs (P,Q) holds
( [x1,y1] in Y1 iff S1[x1,y1] ) ;
A4: for x, y being Element of ConFuncs (P,Q) holds
( [x,y] in Y2 iff S1[x,y] ) by A2;
thus  Y1 = Y2 from RELSET_1:sch_4(A3, A4); ::_thesis: verum
end;
hence  ( ( for x, y being set holds
( [x,y] in Y1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds
( [x,y] in Y2 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) implies Y1 = Y2 ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines ConRelat POSET_1:def_7_:_
 for P, Q being non empty strict chain-complete Poset
for b3 being Relation of (ConFuncs (P,Q)) holds
( b3 = ConRelat (P,Q) iff for x, y being set holds
( [x,y] in b3 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) );

Lm18:  for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q)
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: field (ConRelat (P,Q)) c= ConFuncs (P,Q)
 (ConFuncs (P,Q)) \/ (ConFuncs (P,Q)) c= ConFuncs (P,Q) ;
hence  field (ConRelat (P,Q)) c= ConFuncs (P,Q) by RELSET_1:8; ::_thesis: verum
end;

Lm19:  for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)
set R = ConRelat (P,Q);
 for x being set st x in ConFuncs (P,Q) holds
[x,x] in ConRelat (P,Q)
proof
let x be set ; ::_thesis: ( x in ConFuncs (P,Q) implies [x,x] in ConRelat (P,Q) )
assume A1: x in ConFuncs (P,Q) ; ::_thesis: [x,x] in ConRelat (P,Q)
then consider x1 being Element of Funcs ( the carrier of P, the carrier of Q) such that
A2: x = x1 and
A3: ex f being continuous Function of P,Q st f = x1 ;
consider f being continuous Function of P,Q such that
A4: f = x1 by A3;
 f <= f by Lm15;
hence  [x,x] in ConRelat (P,Q) by A1, A2, A4, Def7; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q) by RELAT_2:def_1; ::_thesis: verum
end;

Lm20:  for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q)
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_transitive_in ConFuncs (P,Q)
set X = ConFuncs (P,Q);
set R = ConRelat (P,Q);
 for x, y, z being set st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) holds
[x,z] in ConRelat (P,Q)
proof
let x, y, z be set ; ::_thesis: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) implies [x,z] in ConRelat (P,Q) )
assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) ) ; ::_thesis: [x,z] in ConRelat (P,Q)
then consider f, g being Function of P,Q such that
A2: ( x = f & y = g & f <= g ) by Def7;
consider g1, h being Function of P,Q such that
A3: ( y = g1 & z = h & g1 <= h ) by A1, Def7;
 f <= h by A3, A2, Lm16;
hence  [x,z] in ConRelat (P,Q) by A1, A2, A3, Def7; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) by RELAT_2:def_8; ::_thesis: verum
end;

Lm21:  for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)
set X = ConFuncs (P,Q);
reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ;
 for x, y being set st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R holds
x = y
proof
let x, y be set ; ::_thesis: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R implies x = y )
assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R ) ; ::_thesis: x = y
then consider f, g being Function of P,Q such that
A2: ( x = f & y = g & f <= g ) by Def7;
consider g1, f1 being Function of P,Q such that
A3: ( y = g1 & x = f1 & g1 <= f1 ) by A1, Def7;
thus  x = y by A2, A3, Lm17; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q) by RELAT_2:def_4; ::_thesis: verum
end;

registration
let P, Q be non empty strict chain-complete Poset;
cluster ConRelat (P,Q) ->  reflexive ;
coherence
 ConRelat (P,Q) is reflexive
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 being set st x in field R holds
[x,x] in R
proof
let x be set ; ::_thesis: ( x in field R implies [x,x] in R )
assume A1: x in field R ; ::_thesis: [x,x] in R
A2: field R c= ConFuncs (P,Q) by Lm18;
 R is_reflexive_in ConFuncs (P,Q) by Lm19;
hence  [x,x] in R by A1, A2, RELAT_2:def_1; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_reflexive_in field (ConRelat (P,Q)) by RELAT_2:def_1; ::_thesis: verum
end;
hence  ConRelat (P,Q) is reflexive by RELAT_2:def_9; ::_thesis: verum
end;
cluster ConRelat (P,Q) ->  transitive ;
coherence
 ConRelat (P,Q) is transitive
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 being set st x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) holds
[x,z] in ConRelat (P,Q)
proof
let x, y, z be set ; ::_thesis: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) implies [x,z] in ConRelat (P,Q) )
assume A3: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & z in field (ConRelat (P,Q)) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) ) ; ::_thesis: [x,z] in ConRelat (P,Q)
set X1 = ConFuncs (P,Q);
A4: field (ConRelat (P,Q)) c= ConFuncs (P,Q) by Lm18;
 ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) by Lm20;
hence  [x,z] in ConRelat (P,Q) by A3, A4, RELAT_2:def_8; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_transitive_in field (ConRelat (P,Q)) by RELAT_2:def_8; ::_thesis: verum
end;
hence  ConRelat (P,Q) is transitive by RELAT_2:def_16; ::_thesis: verum
end;
cluster ConRelat (P,Q) ->  antisymmetric ;
coherence
 ConRelat (P,Q) is antisymmetric
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 being set st x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R holds
x = y
proof
let x, y be set ; ::_thesis: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R implies x = y )
assume A5: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R ) ; ::_thesis: x = y
set X1 = ConFuncs (P,Q);
A6: field R c= ConFuncs (P,Q) by Lm18;
 R is_antisymmetric_in ConFuncs (P,Q) by Lm21;
hence  x = y by A5, A6, RELAT_2:def_4; ::_thesis: verum
end;
hence  ConRelat (P,Q) is_antisymmetric_in field (ConRelat (P,Q)) by RELAT_2:def_4; ::_thesis: verum
end;
hence  ConRelat (P,Q) is antisymmetric by RELAT_2:def_12; ::_thesis: verum
end;
end;

definition
let P, Q be non empty strict chain-complete Poset;
func ConPoset (P,Q) ->  non empty strict Poset equals :: POSET_1:def 8
 RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);
correctness
coherence
RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset;
proof
set IT = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);
A1: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_reflexive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm19;
A2: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_transitive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm20;
 the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_antisymmetric_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm21;
hence  RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset by A1, A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines ConPoset POSET_1:def_8_:_
 for P, Q being non empty strict chain-complete Poset holds ConPoset (P,Q) = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

definition
let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));
let p be Element of P;
funcF -image p ->  non empty Chain of Q equals :: POSET_1:def 9
 {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  ;
correctness
coherence
{  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  is non empty Chain of Q;
proof
set R = the InternalRel of Q;
set IT =  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  ;
 for x being set st x in  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  holds
x in the carrier of Q
proof
let x be set ; ::_thesis: ( x in  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  implies x in the carrier of Q )
assume  x in  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  ; ::_thesis: x in the carrier of Q
then consider a being Element of Q such that
A1: ( x = a & ex f being continuous Function of P,Q st
( f in F & a = f . p ) ) ;
reconsider x = x as Element of the carrier of Q by A1;
 x in the carrier of Q ;
hence  x in the carrier of Q ; ::_thesis: verum
end;
then reconsider IT =  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  as Subset of Q by TARSKI:def_3;
 for x, y being set st x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q holds
[y,x] in the InternalRel of Q
proof
let x, y be set ; ::_thesis: ( x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q implies [y,x] in the InternalRel of Q )
assume A2: ( x in IT & y in IT & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then consider a being Element of Q such that
A3: ( x = a & ex f being continuous Function of P,Q st
( f in F & a = f . p ) ) ;
consider f being continuous Function of P,Q such that
A4: ( f in F & a = f . p ) by A3;
consider b being Element of Q such that
A5: ( y = b & ex g being continuous Function of P,Q st
( g in F & b = g . p ) ) by A2;
consider g being 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: the InternalRel of (ConPoset (P,Q)) is_strongly_connected_in F by ORDERS_2:def_7;
percases ( [f,g] in the InternalRel of (ConPoset (P,Q)) or [g,f] in the InternalRel of (ConPoset (P,Q)) ) by A7, A4, A6, RELAT_2:def_7;
suppose [f,g] in the InternalRel of (ConPoset (P,Q)) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then consider f1, g1 being 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  ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def_5; ::_thesis: verum
end;
suppose [g,f] in the InternalRel of (ConPoset (P,Q)) ; ::_thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then consider g1, f1 being 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  ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
then A10: the InternalRel of Q is_connected_in IT by RELAT_2:def_6;
 for x being set st x in IT holds
[x,x] in the InternalRel of Q
proof
let x be set ; ::_thesis: ( x in IT implies [x,x] in the InternalRel of Q )
assume  x in IT ; ::_thesis: [x,x] in the InternalRel of Q
then reconsider x = x as Element of Q ;
 x <= x ;
hence  [x,x] in the InternalRel of Q by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of Q is_reflexive_in IT by RELAT_2:def_1;
then  the InternalRel of Q is_strongly_connected_in IT by A10, ORDERS_1:7;
then reconsider IT = IT as Chain of Q by ORDERS_2:def_7;
consider a being set  such that
A11: a in F by XBOOLE_0:7;
 a in ConFuncs (P,Q) by A11;
then consider b being Element of Funcs ( the carrier of P, the carrier of Q) such that
A12: ( a = b & ex f being continuous Function of P,Q st f = b ) ;
consider f being 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   {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  is non empty Chain of Q ; ::_thesis: verum
end;
end;

:: deftheorem  defines -image POSET_1:def_9_:_
 for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for p being Element of P holds F -image p =  {  x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p )  }  ;

definition
let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));
func sup_func F ->  Function of P,Q means :Def10: :: POSET_1:def 10
 for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
it . p = sup M;
existence
 ex b1 being Function of P,Q st
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b1 . p = sup M
proof
set X = the carrier of P;
set Y = the carrier of Q;
defpred S1[ set , set ] means  for p being Element of P
for M being non empty Chain of Q st p = $1 & M = F -image p holds
$2 = sup M;
A1: for x being set st x in the carrier of P holds
ex y being set st
( y in the carrier of Q & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of P implies ex y being set st
( y in the carrier of Q & S1[x,y] ) )
assume  x in the carrier of P ; ::_thesis: ex y being set st
( y in the carrier of Q & S1[x,y] )
then reconsider x = x as Element of P ;
reconsider a = F -image x as non empty Chain of Q ;
set y = sup a;
take  sup a ; ::_thesis: ( sup a in the carrier of Q & S1[x, sup a] )
thus  ( sup a in the carrier of Q & S1[x, sup a] ) ; ::_thesis: verum
end;
consider IT being Function of the carrier of P, the carrier of Q such that
A2: for x being set st x in the carrier of P holds
S1[x,IT . x] from FUNCT_2:sch_1(A1);
 for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
IT . p = sup M by A2;
hence  ex b1 being Function of P,Q st
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b1 . p = sup M ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of P,Q st ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b1 . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b2 . p = sup M ) holds
b1 = b2
proof
let f, g be Function of P,Q; ::_thesis: ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g )
 ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g )
proof
assume A3: ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) ) ; ::_thesis: f = g
set X = the carrier of P;
 for x being set st x in the carrier of P holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in the carrier of P implies f . x = g . x )
assume  x in the carrier of P ; ::_thesis: f . x = g . 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  f . x = g . x ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
hence  ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g ) ; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines sup_func POSET_1:def_10_:_
 for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for b4 being Function of P,Q holds
( b4 = sup_func F iff for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b4 . p = sup M );

Lm22:  for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is monotone
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is monotone
let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is monotone
reconsider f = sup_func F as Function of P,Q ;
 for p, p1 being Element of P st p <= p1 holds
for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1
proof
let p, p1 be Element of P; ::_thesis: ( p <= p1 implies for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1 )
assume A1: p <= p1 ; ::_thesis: for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1
 for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1
proof
let q, q1 be Element of Q; ::_thesis: ( q = f . p & q1 = f . p1 implies q <= q1 )
assume A2: ( q = f . p & q1 = f . p1 ) ; ::_thesis: q <= q1
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 being Element of Q st x in X holds
x <= q1
proof
let x be Element of Q; ::_thesis: ( x in X implies x <= q1 )
assume  x in X ; ::_thesis: x <= q1
then consider a being Element of Q such that
A6: ( x = a & ex g being continuous Function of P,Q st
( g in F & a = g . p ) ) ;
consider g being 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, LATTICE3:def_9;
hence  x <= q1 by A6, A8, ORDERS_2:3; ::_thesis: verum
end;
then  X is_<=_than q1 by LATTICE3:def_9;
hence  q <= q1 by A3, A4, YELLOW_0:def_9; ::_thesis: verum
end;
hence  for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1 ; ::_thesis: verum
end;
hence  sup_func F is monotone by ORDERS_3:def_5; ::_thesis: verum
end;

Lm23:  for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q being Element of Q st q in M holds
q <= sup M
proof
let Q be non empty strict chain-complete Poset; ::_thesis: for M being non empty Chain of Q
for q being Element of Q st q in M holds
q <= sup M
let M be non empty Chain of Q; ::_thesis: for q being Element of Q st q in M holds
q <= sup M
let q be Element of Q; ::_thesis: ( q in M implies q <= sup M )
assume A1: q in M ; ::_thesis: q <= sup M
A2: ex_sup_of M,Q by Def1;
set x = sup M;
 M is_<=_than sup M by A2, YELLOW_0:def_9;
hence  q <= sup M by A1, LATTICE3:def_9; ::_thesis: verum
end;

Lm24:  for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
proof
let Q be non empty strict chain-complete Poset; ::_thesis: for M being non empty Chain of Q
for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
let M be non empty Chain of Q; ::_thesis: for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
let q1 be Element of Q; ::_thesis: ( ( for q being Element of Q st q in M holds
q <= q1 ) implies sup M <= q1 )
assume  for q being Element of Q st q in M holds
q <= q1 ; ::_thesis: sup M <= q1
then A1: M is_<=_than q1 by LATTICE3:def_9;
A2: ex_sup_of M,Q by Def1;
thus  sup M <= q1 by A2, A1, YELLOW_0:def_9; ::_thesis: verum
end;

Lm25:  for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous
let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is continuous
reconsider f = sup_func F as monotone Function of P,Q by Lm22;
 for L being non empty Chain of P holds f . (sup L) <= sup (f .: L)
proof
let L be non empty Chain of P; ::_thesis: f . (sup L) <= sup (f .: 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 (sup L);
A1: f . (sup L) = sup (F -image (sup L)) by Def10;
 for q being Element of Q st q in F -image (sup L) holds
q <= sup M1
proof
let q be Element of Q; ::_thesis: ( q in F -image (sup L) implies q <= sup M1 )
assume  q in F -image (sup L) ; ::_thesis: q <= sup M1
then consider q0 being Element of Q such that
A2: ( q = q0 & ex g being continuous Function of P,Q st
( g in F & q0 = g . (sup L) ) ) ;
consider g being continuous Function of P,Q such that
A3: ( g in F & q0 = g . (sup L) ) by A2;
reconsider M2 = g .: L as non empty Chain of Q by Th1;
A4: q = sup M2 by Th6, A2, A3;
 for q2 being Element of Q st q2 in M2 holds
q2 <= sup M1
proof
let q2 be Element of Q; ::_thesis: ( q2 in M2 implies q2 <= sup M1 )
assume  q2 in M2 ; ::_thesis: q2 <= sup M1
then consider x being set  such that
A5: ( x in dom g & x in L & q2 = g . x ) by FUNCT_1:def_6;
reconsider x = x as Element of P by A5;
set Mx = F -image x;
A6: f . x = sup (F -image x) by Def10;
set y = f . x;
 x in the carrier of P ;
then  x in dom f by FUNCT_2:def_1;
then  f . x in M1 by A5, FUNCT_1:def_6;
then A7: f . x <= sup M1 by Lm23;
 q2 in F -image x by A5, A3;
then  q2 <= sup (F -image x) by Lm23;
hence  q2 <= sup M1 by A7, A6, ORDERS_2:3; ::_thesis: verum
end;
hence  q <= sup M1 by A4, Lm24; ::_thesis: verum
end;
hence  f . (sup L) <= sup (f .: L) by A1, Lm24; ::_thesis: verum
end;
hence  sup_func F is continuous by Th8; ::_thesis: verum
end;

registration
let P, Q be non empty strict chain-complete Poset;
let F be non empty Chain of (ConPoset (P,Q));
cluster sup_func F ->  continuous ;
correctness
coherence
sup_func F is continuous ;
by Lm25;
end;

Lm26:  for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is Element of (ConPoset (P,Q))
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is Element of (ConPoset (P,Q))
let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: sup_func F is Element of (ConPoset (P,Q))
set x = sup_func F;
A1: sup_func F 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  sup_func F is Element of (ConPoset (P,Q)) ; ::_thesis: verum
end;

Lm27:  for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for x being set st x in F holds
ex g being continuous Function of P,Q st x = g
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q))
for x being set st x in F holds
ex g being continuous Function of P,Q st x = g
let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: for x being set st x in F holds
ex g being continuous Function of P,Q st x = g
let x be set ; ::_thesis: ( x in F implies ex g being continuous Function of P,Q st x = g )
assume  x in F ; ::_thesis: ex g being continuous Function of P,Q st x = g
then  x in ConFuncs (P,Q) ;
then consider y being Element of Funcs ( the carrier of P, the carrier of Q) such that
A1: ( x = y & ex g being continuous Function of P,Q st g = y ) ;
thus  ex g being continuous Function of P,Q st x = g by A1; ::_thesis: verum
end;

theorem Th11: :: POSET_1:11
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for F being non empty Chain of (ConPoset (P,Q)) holds
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
let F be non empty Chain of (ConPoset (P,Q)); ::_thesis: ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
set X = ConPoset (P,Q);
set f1 = sup_func F;
reconsider f = sup_func F as Element of (ConPoset (P,Q)) by Lm26;
 for x being Element of (ConPoset (P,Q)) st x in F holds
x <= f
proof
let x be Element of (ConPoset (P,Q)); ::_thesis: ( x in F implies x <= f )
assume A1: x in F ; ::_thesis: x <= f
then consider g1 being continuous Function of P,Q such that
A2: x = g1 by Lm27;
reconsider g = g1 as Element of (ConPoset (P,Q)) by A2;
 for p being Element of P holds g1 . p <= (sup_func F) . p
proof
let p be Element of P; ::_thesis: g1 . p <= (sup_func F) . p
 for q1, q2 being Element of Q st q1 = g1 . p & q2 = (sup_func F) . p holds
q1 <= q2
proof
let q1, q2 be Element of Q; ::_thesis: ( q1 = g1 . p & q2 = (sup_func F) . p implies q1 <= q2 )
assume A3: ( q1 = g1 . p & q2 = (sup_func F) . p ) ; ::_thesis: q1 <= q2
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  q1 <= q2 by A4, Lm23; ::_thesis: verum
end;
hence  g1 . p <= (sup_func F) . p ; ::_thesis: verum
end;
then  g1 <= sup_func F by YELLOW_2:9;
then  [g,f] in ConRelat (P,Q) by Def7;
hence  x <= f by A2, ORDERS_2:def_5; ::_thesis: verum
end;
then A5: F is_<=_than f by LATTICE3:def_9;
 for y being Element of (ConPoset (P,Q)) st F is_<=_than y holds
f <= y
proof
let y be Element of (ConPoset (P,Q)); ::_thesis: ( F is_<=_than y implies f <= y )
 y in ConFuncs (P,Q) ;
then consider y1 being Element of Funcs ( the carrier of P, the carrier of Q) such that
A6: ( y = y1 & ex gy being continuous Function of P,Q st gy = y1 ) ;
consider gy being 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 ; ::_thesis: f <= y
 for p being Element of P holds (sup_func F) . p <= gy . p
proof
let p be Element of P; ::_thesis: (sup_func F) . p <= gy . p
 for q1, q2 being Element of Q st q1 = (sup_func F) . p & q2 = gy . p holds
q1 <= q2
proof
let q1, q2 be Element of Q; ::_thesis: ( q1 = (sup_func F) . p & q2 = gy . p implies q1 <= q2 )
assume A9: ( q1 = (sup_func F) . p & q2 = gy . p ) ; ::_thesis: q1 <= q2
reconsider M = F -image p as non empty Chain of Q ;
 for q being Element of Q st q in M holds
q <= q2
proof
let q be Element of Q; ::_thesis: ( q in M implies q <= q2 )
assume  q in M ; ::_thesis: q <= q2
then consider a being Element of Q such that
A10: ( q = a & ex g being continuous Function of P,Q st
( g in F & a = g . p ) ) ;
consider g being 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, LATTICE3:def_9;
then  [g1,y] in ConRelat (P,Q) by ORDERS_2:def_5;
then consider g2, g3 being Function of P,Q such that
A12: ( g1 = g2 & y = g3 & g2 <= g3 ) by Def7;
thus  q <= q2 by A12, A6, A7, A10, A11, A9, YELLOW_2:9; ::_thesis: verum
end;
then  sup M <= q2 by Lm24;
hence  q1 <= q2 by A9, Def10; ::_thesis: verum
end;
hence  (sup_func F) . p <= gy . p ; ::_thesis: verum
end;
then  sup_func F <= gy by YELLOW_2:9;
then  [f,y] in ConRelat (P,Q) by A6, A7, Def7;
hence  f <= y by ORDERS_2:def_5; ::_thesis: verum
end;
hence  ( F is_<=_than y implies f <= y ) ; ::_thesis: verum
end;
hence  ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) ) by A5, YELLOW_0:30; ::_thesis: verum
end;

definition
let P, Q be non empty strict chain-complete Poset;
func min_func (P,Q) ->  Function of P,Q equals :: POSET_1:def 11
P --> (Bottom Q);
coherence
 P --> (Bottom Q) is Function of P,Q ;
end;

:: deftheorem  defines min_func POSET_1:def_11_:_
 for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) = P --> (Bottom Q);

registration
let P, Q be non empty strict chain-complete Poset;
cluster min_func (P,Q) ->  continuous ;
coherence
 min_func (P,Q) is continuous by Th7;
end;

Lm28:  for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q))
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: min_func (P,Q) is Element of (ConPoset (P,Q))
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  min_func (P,Q) is Element of (ConPoset (P,Q)) ; ::_thesis: verum
end;

theorem Th12: :: POSET_1:12
for P, Q being non empty strict chain-complete Poset
for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds
f is_<=_than the carrier of (ConPoset (P,Q))
proof
let P, Q be non empty strict chain-complete Poset; ::_thesis: for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds
f is_<=_than the carrier of (ConPoset (P,Q))
let f be Element of (ConPoset (P,Q)); ::_thesis: ( f = min_func (P,Q) implies f is_<=_than the carrier of (ConPoset (P,Q)) )
assume A1: f = min_func (P,Q) ; ::_thesis: f is_<=_than the carrier of (ConPoset (P,Q))
set f1 = min_func (P,Q);
 for x being Element of (ConPoset (P,Q)) holds f <= x
proof
let x be Element of (ConPoset (P,Q)); ::_thesis: f <= x
 x in ConFuncs (P,Q) ;
then consider x1 being Element of Funcs ( the carrier of P, the carrier of Q) such that
A2: ( x = x1 & ex g being continuous Function of P,Q st g = x1 ) ;
consider g being continuous Function of P,Q such that
A3: g = x1 by A2;
 for p being Element of P holds (min_func (P,Q)) . p <= g . p
proof
let p be Element of P; ::_thesis: (min_func (P,Q)) . p <= g . p
 for q1, q2 being Element of Q st q1 = (min_func (P,Q)) . p & q2 = g . p holds
q1 <= q2
proof
let q1, q2 be Element of Q; ::_thesis: ( q1 = (min_func (P,Q)) . p & q2 = g . p implies q1 <= q2 )
assume  ( q1 = (min_func (P,Q)) . p & q2 = g . p ) ; ::_thesis: q1 <= q2
then  q1 = Bottom Q by FUNCOP_1:7;
hence  q1 <= q2 by YELLOW_0:44; ::_thesis: verum
end;
hence  (min_func (P,Q)) . p <= g . p ; ::_thesis: verum
end;
then  min_func (P,Q) <= g by YELLOW_2:9;
then  [f,x] in ConRelat (P,Q) by A2, A3, Def7, A1;
hence  f <= x by ORDERS_2:def_5; ::_thesis: verum
end;
hence  f is_<=_than the carrier of (ConPoset (P,Q)) by Lm4; ::_thesis: verum
end;

registration
let P, Q be non empty strict chain-complete Poset;
cluster ConPoset (P,Q) ->  non empty strict chain-complete ;
coherence
 ConPoset (P,Q) is chain-complete
proof
set IT = ConPoset (P,Q);
 ex a being Element of (ConPoset (P,Q)) st a is_<=_than the carrier of (ConPoset (P,Q))
proof
reconsider a = min_func (P,Q) as Element of (ConPoset (P,Q)) by Lm28;
take  a ; ::_thesis: a is_<=_than the carrier of (ConPoset (P,Q))
thus  a is_<=_than the carrier of (ConPoset (P,Q)) by Th12; ::_thesis: verum
end;
then A1: ConPoset (P,Q) is lower-bounded by YELLOW_0:def_4;
 for L being Chain of (ConPoset (P,Q)) st not L is empty holds
ex_sup_of L, ConPoset (P,Q) by Th11;
hence  ConPoset (P,Q) is chain-complete by Def1, A1; ::_thesis: verum
end;
end;

begin

Lm29:  for x being set
for P being non empty strict chain-complete Poset st x is Element of (ConPoset (P,P)) holds
x is continuous Function of P,P
proof
let x be set ; ::_thesis: for P being non empty strict chain-complete Poset st x is Element of (ConPoset (P,P)) holds
x is continuous Function of P,P
let P be non empty strict chain-complete Poset; ::_thesis: ( x is Element of (ConPoset (P,P)) implies x is continuous Function of P,P )
assume  x is Element of (ConPoset (P,P)) ; ::_thesis: x is continuous Function of P,P
then  x in ConFuncs (P,P) ;
then consider y being Element of Funcs ( the carrier of P, the carrier of P) such that
A1: ( x = y & ex g being continuous Function of P,P st g = y ) ;
thus  x is continuous Function of P,P by A1; ::_thesis: verum
end;

Lm30:  for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous Function of P,P holds
g is Element of (ConPoset (P,P))
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g being monotone Function of P,P st g is continuous Function of P,P holds
g is Element of (ConPoset (P,P))
let g be monotone Function of P,P; ::_thesis: ( g is continuous Function of P,P implies g is Element of (ConPoset (P,P)) )
assume A1: g is continuous Function of P,P ; ::_thesis: g is Element of (ConPoset (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  g is Element of (ConPoset (P,P)) ; ::_thesis: verum
end;

definition
let P be non empty strict chain-complete Poset;
func fix_func P ->  Function of (ConPoset (P,P)),P means :Def12: :: POSET_1:def 12
 for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
it . g = least_fix_point h;
existence
 ex b1 being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h
proof
set X = the carrier of (ConPoset (P,P));
set Y = the carrier of P;
defpred S1[ set , set ] means  for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h & g = $1 holds
$2 = least_fix_point h;
A1: for x being set st x in the carrier of (ConPoset (P,P)) holds
ex y being set st
( y in the carrier of P & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (ConPoset (P,P)) implies ex y being set st
( y in the carrier of P & S1[x,y] ) )
assume  x in the carrier of (ConPoset (P,P)) ; ::_thesis: ex y being set st
( y in the carrier of P & S1[x,y] )
then reconsider x = x as Element of (ConPoset (P,P)) ;
reconsider h = x as continuous Function of P,P by Lm29;
take  least_fix_point h ; ::_thesis: ( least_fix_point h in the carrier of P & S1[x, least_fix_point h] )
thus  ( least_fix_point h in the carrier of P & S1[x, least_fix_point h] ) ; ::_thesis: verum
end;
consider IT being Function of the carrier of (ConPoset (P,P)), the carrier of P such that
A2: for x being set st x in the carrier of (ConPoset (P,P)) holds
S1[x,IT . x] from FUNCT_2:sch_1(A1);
 for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
IT . g = least_fix_point h by A2;
hence  ex b1 being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (ConPoset (P,P)),P st ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h ) & ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b2 . g = least_fix_point h ) holds
b1 = b2
proof
let h1, h2 be Function of (ConPoset (P,P)),P; ::_thesis: ( ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
h1 . g = least_fix_point h ) & ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
h2 . g = least_fix_point h ) implies h1 = h2 )
assume A3: ( ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
h1 . g = least_fix_point h ) & ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
h2 . g = least_fix_point h ) ) ; ::_thesis: h1 = h2
set X = the carrier of (ConPoset (P,P));
 for x being set st x in the carrier of (ConPoset (P,P)) holds
h1 . x = h2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of (ConPoset (P,P)) implies h1 . x = h2 . x )
assume  x in the carrier of (ConPoset (P,P)) ; ::_thesis: h1 . x = h2 . x
then reconsider g = x as Element of (ConPoset (P,P)) ;
reconsider h = g as continuous Function of P,P by Lm29;
h1 . x = least_fix_point h by A3
.= h2 . x by A3 ;
hence  h1 . x = h2 . x ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines fix_func POSET_1:def_12_:_
 for P being non empty strict chain-complete Poset
for b2 being Function of (ConPoset (P,P)),P holds
( b2 = fix_func P iff for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b2 . g = least_fix_point h );

Lm31:  for P being non empty strict chain-complete Poset
for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
proof
let P be non empty strict chain-complete Poset; ::_thesis: for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
let p1, p2 be Element of (ConPoset (P,P)); ::_thesis: ( p1 <= p2 implies ( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) ) )
assume  p1 <= p2 ; ::_thesis: ( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
then A1: [p1,p2] in ConRelat (P,P) by ORDERS_2:def_5;
 ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 )
proof
consider g1, g2 being 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 Lm29;
 g1 = h1 by A2;
then reconsider g1 = g1 as continuous Function of P,P ;
 g2 = h2 by A2;
then reconsider g2 = g2 as continuous Function of P,P ;
take  g1 ; ::_thesis: ex g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 )
take  g2 ; ::_thesis: ( p1 = g1 & p2 = g2 & g1 <= g2 )
thus  ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A2; ::_thesis: verum
end;
hence  ( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) ) ; ::_thesis: verum
end;

Lm32:  for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P
proof
let P be non empty strict chain-complete Poset; ::_thesis: fix_func P is monotone Function of (ConPoset (P,P)),P
set IT = fix_func P;
 for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b
proof
let p1, p2 be Element of (ConPoset (P,P)); ::_thesis: ( p1 <= p2 implies for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b )
assume A1: p1 <= p2 ; ::_thesis: for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b
let a, b be Element of P; ::_thesis: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 implies a <= b )
assume A2: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 ) ; ::_thesis: a <= b
consider g1, g2 being continuous Function of P,P such that
A3: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, Lm31;
 ( a = least_fix_point g1 & b = least_fix_point g2 ) by A2, Def12, A3;
hence  a <= b by A3, Th10; ::_thesis: verum
end;
hence  fix_func P is monotone Function of (ConPoset (P,P)),P by ORDERS_3:def_5; ::_thesis: verum
end;

Lm33:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X, x being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
proof
let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X, x being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for n being Nat
for X, x being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let n be Nat; ::_thesis: for X, x being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let X, x be set ; ::_thesis: ( X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X implies ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) ) )
assume  ( X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X ) ; ::_thesis: ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
then consider p being Element of P such that
A1: ( x = p & ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) ) ;
thus  ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) ) by A1; ::_thesis: verum
end;

Lm34:  for x being set
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
x is Element of P
proof
let x be set ; ::_thesis: for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
x is Element of P
let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
x is Element of P
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
x is Element of P
let n be Nat; ::_thesis: for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in X holds
x is Element of P
let X be set ; ::_thesis: ( X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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 )
assume A1: X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  ; ::_thesis: ( not x in X or x is Element of P )
 ( x in X implies x is Element of P )
proof
assume  x in X ; ::_thesis: x is Element of P
then consider p being Element of P such that
A2: ( x = p & ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) ) by A1;
thus  x is Element of P by A2; ::_thesis: verum
end;
hence  ( not x in X or x is Element of P ) ; ::_thesis: verum
end;

Lm35:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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 P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let n be Nat; ::_thesis: for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let X be set ; ::_thesis: ( X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  implies X is non empty Subset of P )
assume A1: X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  ; ::_thesis: X is non empty Subset of P
consider g being set  such that
A2: g in G by XBOOLE_0:def_1;
reconsider g = g as Element of (ConPoset (P,P)) by A2;
reconsider gg = g as continuous Function of P,P by Lm29;
reconsider p = (iter (gg,n)) . (Bottom P) as Element of P by Lm6;
A3: p in X by A1, A2;
 for x being set st x in X holds
x in the carrier of P
proof
let x be set ; ::_thesis: ( x in X implies x in the carrier of P )
assume  x in X ; ::_thesis: x in the carrier of P
then  x is Element of the carrier of P by Lm34, A1;
hence  x in the carrier of P ; ::_thesis: verum
end;
hence  X is non empty Subset of P by A3, TARSKI:def_3; ::_thesis: verum
end;

Lm36:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
proof
let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
let f, g be monotone Function of P,P; ::_thesis: ( f in G & g in G & not f <= g implies g <= f )
assume A1: ( f in G & g in G ) ; ::_thesis: ( f <= g or g <= f )
set S = the InternalRel of (ConPoset (P,P));
A2: the InternalRel of (ConPoset (P,P)) is_strongly_connected_in G by ORDERS_2:def_7;
percases ( [f,g] in the InternalRel of (ConPoset (P,P)) or [g,f] in the InternalRel of (ConPoset (P,P)) ) by A2, A1, RELAT_2:def_7;
suppose [f,g] in the InternalRel of (ConPoset (P,P)) ; ::_thesis: ( f <= g or g <= f )
then consider f1, g1 being Function of P,P such that
A3: ( f = f1 & g = g1 & f1 <= g1 ) by Def7;
thus  ( f <= g or g <= f ) by A3; ::_thesis: verum
end;
suppose [g,f] in the InternalRel of (ConPoset (P,P)) ; ::_thesis: ( f <= g or g <= f )
then consider g1, f1 being Function of P,P such that
A4: ( g = g1 & f = f1 & g1 <= f1 ) by Def7;
thus  ( f <= g or g <= f ) by A4; ::_thesis: verum
end;
end;
end;

Lm37:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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 P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for n being Nat
for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let n be Nat; ::_thesis: for X being set st X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being 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
let X be set ; ::_thesis: ( X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  implies X is non empty Chain of P )
assume A1: X =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  ; ::_thesis: X is non empty Chain of P
set R = the InternalRel of P;
reconsider X = X as non empty Subset of P by A1, Lm35;
 for x, y being set st x in X & y in X & x <> y & not [x,y] in the InternalRel of P holds
[y,x] in the InternalRel of P
proof
let x, y be set ; ::_thesis: ( x in X & y in X & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P )
assume A2: ( x in X & y in X & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then consider p1 being Element of P, g1 being continuous Function of P,P such that
A3: ( x = p1 & g1 in G & p1 = (iter (g1,n)) . (Bottom P) ) by A1, Lm33;
consider p2 being Element of P, g2 being continuous Function of P,P such that
A4: ( y = p2 & g2 in G & p2 = (iter (g2,n)) . (Bottom P) ) by A1, A2, Lm33;
percases ( g1 <= g2 or g2 <= g1 ) by A3, A4, Lm36;
suppose g1 <= g2 ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then  p1 <= p2 by Lm12, A3, A4;
hence  ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def_5; ::_thesis: verum
end;
suppose g2 <= g1 ; ::_thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then  p2 <= p1 by Lm12, A3, A4;
hence  ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
then A5: the InternalRel of P is_connected_in X by RELAT_2:def_6;
 for x being set st x in X holds
[x,x] in the InternalRel of P
proof
let x be set ; ::_thesis: ( x in X implies [x,x] in the InternalRel of P )
assume  x in X ; ::_thesis: [x,x] in the InternalRel of P
then reconsider x = x as Element of P ;
 x <= x ;
hence  [x,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of P is_reflexive_in X by RELAT_2:def_1;
then  the InternalRel of P is_strongly_connected_in X by A5, ORDERS_1:7;
hence  X is non empty Chain of P by ORDERS_2:def_7; ::_thesis: verum
end;

Lm38:  for P being non empty strict chain-complete Poset
for h being Function of (ConPoset (P,P)),P
for G being non empty Chain of (ConPoset (P,P))
for x being set st x in G holds
h . x in h .: G
proof
let P be non empty strict chain-complete Poset; ::_thesis: for h being Function of (ConPoset (P,P)),P
for G being non empty Chain of (ConPoset (P,P))
for x being set st x in G holds
h . x in h .: G
let h be Function of (ConPoset (P,P)),P; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for x being set st x in G holds
h . x in h .: G
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for x being set st x in G holds
h . x in h .: G
let x be set ; ::_thesis: ( x in G implies h . x in h .: G )
assume A1: x in G ; ::_thesis: h . x in h .: G
set X = the carrier of (ConPoset (P,P));
set Y = the carrier of P;
reconsider h = h as Function of the carrier of (ConPoset (P,P)), the carrier of P ;
 x in the carrier of (ConPoset (P,P)) by A1;
then  x in dom h by FUNCT_2:def_1;
hence  h . x in h .: G by A1, FUNCT_1:def_6; ::_thesis: verum
end;

Lm39:  for P being non empty strict chain-complete Poset
for g being continuous Function of P,P
for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
proof
let P be non empty strict chain-complete Poset; ::_thesis: for g being continuous Function of P,P
for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let g be continuous Function of P,P; ::_thesis: for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let p, p1 be Element of P; ::_thesis: for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let n be Nat; ::_thesis: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) implies p1 <= p )
set a = Bottom P;
assume A1: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) ) ; ::_thesis: p1 <= p
then A2: p1 in iterSet (g,(Bottom P)) ;
reconsider g1 = g as Element of (ConPoset (P,P)) by Lm30;
reconsider G1 = g1 as continuous Function of P,P ;
p = least_fix_point G1 by Def12, A1
.= sup (iter_min g) by Th9 ;
hence  p1 <= p by Lm23, A2; ::_thesis: verum
end;

Lm40:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
proof
let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P))
for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
let x be set ; ::_thesis: for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
let n be Nat; ::_thesis: for M being non empty Chain of P
for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
let M be non empty Chain of P; ::_thesis: for g1 being monotone Function of P,P st M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
let g1 be monotone Function of P,P; ::_thesis: ( M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M implies ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) ) )
assume A1: ( M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) )  }  & x in g1 .: M ) ; ::_thesis: ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
then  ex y being set st
( y in dom g1 & y in M & x = g1 . y ) by FUNCT_1:def_6;
then consider y being Element of M such that
A2: ( y in M & x = g1 . y ) ;
consider p being Element of P such that
A3: ( y = p & ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) ) by A1, A2;
thus  ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) ) by A2, A3; ::_thesis: verum
end;

Lm41:  for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
proof
let P be non empty strict chain-complete Poset; ::_thesis: for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
let G be non empty Chain of (ConPoset (P,P)); ::_thesis: (fix_func P) . (sup G) <= sup ((fix_func P) .: G)
reconsider h = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm32;
 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 . (sup G);
reconsider G0 = sup G as continuous Function of P,P by Lm29;
A1: h . (sup G) = least_fix_point G0 by Def12;
A2: sup G = sup_func G by Th11;
then reconsider g0 = sup G as continuous Function of P,P ;
set a = Bottom P;
reconsider I0 = iterSet (g0,(Bottom P)) as non empty Chain of P by Th3;
A3: h . (sup G) = sup (iter_min g0) by Th9, A1
.= sup I0 ;
A4: ex_sup_of I0,P by Def1;
 for x being Element of P st x in I0 holds
x <= sup L
proof
let x be Element of P; ::_thesis: ( x in I0 implies x <= sup L )
assume  x in I0 ; ::_thesis: x <= sup L
then consider y being Element of P such that
A5: ( x = y & ex n being Nat st y = (iter (g0,n)) . (Bottom P) ) ;
consider n0 being Nat such that
A6: x = (iter (g0,n0)) . (Bottom P) by A5;
set M0 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n0)) . (Bottom P) )  }  ;
reconsider M0 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n0)) . (Bottom P) )  }  as non empty Chain of P by Lm37;
 for p being Element of P st p in M0 holds
p <= sup L
proof
let p be Element of P; ::_thesis: ( p in M0 implies p <= sup L )
assume  p in M0 ; ::_thesis: p <= sup L
then consider p0 being Element of P, g being continuous Function of P,P such that
A7: ( p = p0 & g in G & p0 = (iter (g,n0)) . (Bottom P) ) by Lm33;
set r = h . g;
 h . g in L by A7, Lm38;
then reconsider r = h . g as Element of P ;
A8: r <= sup L by Lm23, A7, Lm38;
 p <= r by A7, Lm39;
hence  p <= sup L by A8, ORDERS_2:3; ::_thesis: verum
end;
then A9: sup M0 <= sup L by Lm24;
defpred S1[ Nat] means  for z being Element of P
for M being non empty Chain of P st z = (iter (g0,$1)) . (Bottom P) & M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,$1)) . (Bottom P) )  }  holds
z <= sup M;
A10: S1[ 0 ]
proof
let z be Element of P; ::_thesis: for M being non empty Chain of P st z = (iter (g0,0)) . (Bottom P) & M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) )  }  holds
z <= sup M
let M be non empty Chain of P; ::_thesis: ( z = (iter (g0,0)) . (Bottom P) & M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) )  }  implies z <= sup M )
assume  z = (iter (g0,0)) . (Bottom P) ; ::_thesis: ( not M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) )  }  or z <= sup M )
then  z = Bottom P by Lm5;
hence  ( not M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,0)) . (Bottom P) )  }  or z <= sup M ) by YELLOW_0:44; ::_thesis: verum
end;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; ::_thesis: S1[k + 1]
 for z1 being Element of P
for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) )  }  holds
z1 <= sup M1
proof
let z1 be Element of P; ::_thesis: for M1 being non empty Chain of P st z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) )  }  holds
z1 <= sup M1
let M1 be non empty Chain of P; ::_thesis: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) )  }  implies z1 <= sup M1 )
assume A13: ( z1 = (iter (g0,(k + 1))) . (Bottom P) & M1 =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,(k + 1))) . (Bottom P) )  }  ) ; ::_thesis: z1 <= sup M1
reconsider z = (iter (g0,k)) . (Bottom P) as Element of P by Lm6;
A14: z1 = (g0 * (iter (g0,k))) . (Bottom P) by A13, FUNCT_7:71
.= g0 . z by Lm7 ;
reconsider M =  {  p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,k)) . (Bottom P) )  }  as non empty Chain of P by Lm37;
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 being Element of P st q in M0 holds
q <= sup M1
proof
let q be Element of P; ::_thesis: ( q in M0 implies q <= sup M1 )
assume  q in M0 ; ::_thesis: q <= sup M1
then consider g being continuous Function of P,P such that
A17: ( g in G & q = g0 . ((iter (g,k)) . (Bottom P)) ) by Lm40;
reconsider a1 = (iter (g,k)) . (Bottom P) as Element of P by Lm6;
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 being Element of P st q1 in W holds
q1 <= sup M1
proof
let q1 be Element of P; ::_thesis: ( q1 in W implies q1 <= sup M1 )
assume  q1 in W ; ::_thesis: q1 <= sup M1
then consider q2 being Element of P such that
A20: ( q1 = q2 & ex g1 being continuous Function of P,P st
( g1 in G & q2 = g1 . a1 ) ) ;
consider g1 being continuous Function of P,P such that
A21: ( g1 in G & q1 = g1 . a1 ) by A20;
percases ( g1 <= g or g <= g1 ) by A17, A21, Lm36;
suppose g1 <= g ; ::_thesis: q1 <= sup M1
then A22: q1 <= g . a1 by A21, YELLOW_2:9;
set a2 = g . a1;
reconsider g2 = g as Element of (ConPoset (P,P)) by Lm30;
reconsider gg = g2 as continuous Function of P,P ;
g . a1 = (g * (iter (g,k))) . (Bottom P) by Lm7
.= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ;
then  g . a1 in M1 by A13, A17;
then  g . a1 <= sup M1 by Lm23;
hence  q1 <= sup M1 by A22, ORDERS_2:3; ::_thesis: verum
end;
supposeA23: g <= g1 ; ::_thesis: q1 <= sup M1
reconsider a2 = (iter (g1,k)) . (Bottom P) as Element of P by Lm6;
 a1 <= a2 by A23, Lm12;
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 Lm30;
reconsider gg = g2 as continuous Function of P,P ;
g1 . a2 = (g1 * (iter (g1,k))) . (Bottom P) by Lm7
.= (iter (gg,(k + 1))) . (Bottom P) by FUNCT_7:71 ;
then  g1 . a2 in M1 by A13, A21;
then  g1 . a2 <= sup M1 by Lm23;
hence  q1 <= sup M1 by A24, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
then  W is_<=_than sup M1 by LATTICE3:def_9;
hence  q <= sup M1 by A18, A19, YELLOW_0:def_9; ::_thesis: verum
end;
then  M0 is_<=_than sup M1 by LATTICE3:def_9;
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  z1 <= sup M1 by A25, ORDERS_2:3; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A10, A11);
then  x <= sup M0 by A6;
hence  x <= sup L by A9, ORDERS_2:3; ::_thesis: verum
end;
then  I0 is_<=_than sup L by LATTICE3:def_9;
hence  h . (sup G) <= sup (h .: G) by A3, A4, YELLOW_0:def_9; ::_thesis: verum
end;
hence  (fix_func P) . (sup G) <= sup ((fix_func P) .: G) ; ::_thesis: verum
end;

registration
let P be non empty strict chain-complete Poset;
cluster fix_func P ->  continuous ;
coherence
 fix_func P is continuous
proof
reconsider f = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm32;
 for L being non empty Chain of (ConPoset (P,P)) holds f . (sup L) <= sup (f .: L) by Lm41;
hence  fix_func P is continuous by Th8; ::_thesis: verum
end;
end;