:: POSET_1 semantic presentation

begin

registration
let P be ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ;
cluster non empty strongly_connected for ( ( ) ( ) Element of K19( the carrier of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( ) ( ) RelStr ) ;
attr IT is chain-complete means :: POSET_1:def 1
( IT : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) is lower-bounded & ( for L being ( ( strongly_connected ) ( strongly_connected ) Chain of IT : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) ) st not L : ( ( strongly_connected ) ( strongly_connected ) Chain of IT : ( ( ) ( ) RelStr ) ) is empty holds
ex_sup_of L : ( ( strongly_connected ) ( strongly_connected ) Chain of IT : ( ( ) ( ) RelStr ) ) ,IT : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) ) );
end;

theorem :: POSET_1:1
for P1, P2 being ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset)
for K being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) )
for h being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds h : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: K : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ) ;

registration
cluster non empty strict V55() reflexive transitive antisymmetric chain-complete for ( ( ) ( ) RelStr ) ;
end;

registration
cluster chain-complete -> lower-bounded for ( ( ) ( ) RelStr ) ;
end;

theorem :: POSET_1:2
for P, Q being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for L being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) )
for f being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds sup (f : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) <= f : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . (sup L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let P be ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ;
let g be ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func iterSet (g,p) -> ( ( non empty ) ( non empty ) set ) equals :: POSET_1:def 2
 { x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex n being ( ( V30() ) ( V24() V25() V26() V30() V117() ext-real non negative V121() ) Nat) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (iter (g : ( ( ) ( ) set ) ,n : ( ( V30() ) ( V24() V25() V26() V30() V117() ext-real non negative V121() ) Nat) )) : ( ( Relation-like ) ( Relation-like ) set ) . p : ( ( ) ( Relation-like g : ( ( ) ( ) set ) -defined g : ( ( ) ( ) set ) -valued ) Element of K19(K20(g : ( ( ) ( ) set ) ,g : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } ;
end;

theorem :: POSET_1:3
for P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for g being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds iterSet (g : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,(Bottom P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) set ) is ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ;

definition
let P be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
let g be ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
func iter_min g -> ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) ) equals :: POSET_1:def 3
 iterSet (g : ( ( ) ( ) set ) ,(Bottom P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) ) : ( ( ) ( ) Element of the carrier of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) set ) ;
end;

theorem :: POSET_1:4
for P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for g being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds sup (iter_min g : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) = sup (g : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: (iter_min g : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ;

theorem :: POSET_1:5
for P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for g1, g2 being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g1 : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g2 : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
sup (iter_min g1 : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) <= sup (iter_min g2 : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ;

definition
let P, Q be ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is continuous means :: POSET_1:def 4
( f : ( ( ) ( Relation-like Q : ( ( ) ( ) set ) -defined Q : ( ( ) ( ) set ) -valued ) Element of K19(K20(Q : ( ( ) ( ) set ) ,Q : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is monotone & ( for L being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) RelStr ) ) holds f : ( ( ) ( Relation-like Q : ( ( ) ( ) set ) -defined Q : ( ( ) ( ) set ) -valued ) Element of K19(K20(Q : ( ( ) ( ) set ) ,Q : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) preserves_sup_of L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty reflexive transitive antisymmetric ) ( non empty V55() reflexive transitive antisymmetric ) Poset) ) ) );
end;

theorem :: POSET_1:6
for P, Q being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous iff ( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone & ( for L being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . (sup L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) = sup (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: POSET_1:7
for Q, P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) --> z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Element of K19(K20( the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total continuous for ( ( ) ( ) Element of K19(K20( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster Function-like quasi_total continuous -> Function-like quasi_total monotone for ( ( ) ( ) Element of K19(K20( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: POSET_1:8
for P, Q being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for f being ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st ( for L being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) holds f : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . (sup L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) <= sup (f : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: L : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

definition
let P be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
let g be ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
assume g : ( ( Function-like quasi_total monotone ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;
func least_fix_point g -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) means :: POSET_1:def 5
( it : ( ( ) ( Relation-like g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -valued ) Element of K19(K20(g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is_a_fixpoint_of g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) & ( for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_fixpoint_of g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) holds
it : ( ( ) ( Relation-like g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -valued ) Element of K19(K20(g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,g : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: POSET_1:9
for P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for g being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds least_fix_point g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup (iter_min g : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ;

theorem :: POSET_1:10
for P being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for g1, g2 being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g1 : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g2 : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
least_fix_point g1 : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= least_fix_point g2 : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

begin

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
func ConFuncs (P,Q) -> ( ( non empty ) ( non empty ) set ) equals :: POSET_1:def 6
 { x : ( ( ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs ( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ) where x is ( ( ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs ( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) : ex f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = x : ( ( ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs ( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) ) ) } ;
end;

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
func ConRelat (P,Q) -> ( ( ) ( Relation-like ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -defined ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) means :: POSET_1:def 7
 for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in it : ( ( ) ( Relation-like Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -valued ) Element of K19(K20(Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) iff ( x : ( ( ) ( ) set ) in ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) set ) in ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) & ex f, g being ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) set ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) set ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ) );
end;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster ConRelat (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -defined ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) -> reflexive ;
cluster ConRelat (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -defined ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) -> transitive ;
cluster ConRelat (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -defined ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) -> antisymmetric ;
end;

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
func ConPoset (P,Q) -> ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) equals :: POSET_1:def 8
 RelStr(# (ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) )) : ( ( non empty ) ( non empty ) set ) ,(ConRelat (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) )) : ( ( ) ( Relation-like ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -defined ConFuncs (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty ) ( non empty ) set ) -valued reflexive antisymmetric transitive ) Relation of ) #) : ( ( strict ) ( non empty strict ) RelStr ) ;
end;

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
let F be ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func F -image p -> ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) equals :: POSET_1:def 9
 { x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) in F : ( ( ) ( Relation-like Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -valued ) Element of K19(K20(Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p : ( ( Function-like quasi_total ) ( Relation-like Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of K19(K20(Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) , the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) } ;
end;

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
let F be ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) ;
func sup_func F -> ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: POSET_1:def 10
 for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for M being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) st M : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) = F : ( ( ) ( Relation-like Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -valued ) Element of K19(K20(Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) -image p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) holds
it : ( ( Function-like quasi_total ) ( Relation-like Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of K19(K20(Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) , the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) = sup M : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( ) ( ) Element of the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
let F be ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) ;
cluster sup_func F : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Element of K19( the carrier of (ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: POSET_1:11
for P, Q being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for F being ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) holds
( ex_sup_of F : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) , ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) & sup_func F : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = "\/" (F : ( ( non empty strongly_connected ) ( non empty strongly_connected ) Chain of ConPoset (b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) ,(ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) ) : ( ( ) ( ) Element of the carrier of (ConPoset (b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) ) ;

definition
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
func min_func (P,Q) -> ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) equals :: POSET_1:def 11
P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) --> (Bottom Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( ) ( ) Element of the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone ) Element of K19(K20( the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster min_func (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: POSET_1:12
for P, Q being ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset)
for f being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = min_func (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_<=_than the carrier of (ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ;

registration
let P, Q be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,Q : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric ) Poset) -> non empty strict reflexive transitive antisymmetric chain-complete ;
end;

begin

definition
let P be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
func fix_func P -> ( ( Function-like quasi_total ) ( Relation-like the carrier of (ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: POSET_1:def 12
 for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for h being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
it : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) . g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) = least_fix_point h : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total monotone continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

registration
let P be ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) ;
cluster fix_func P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (ConPoset (P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) ,P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) )) : ( ( non empty strict reflexive transitive antisymmetric ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of P : ( ( non empty strict reflexive transitive antisymmetric chain-complete ) ( non empty strict V55() reflexive transitive antisymmetric lower-bounded chain-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total continuous ;
end;