(def-constant set%prec 
    "lambda(a,b:sets[ind_1], a subseteq b)"
    (theory generic-theory-1))
	    	            

(def-theorem ()
    "forall(a,c:sets[ind_1],
          forsome(b:sets[ind_1],a set%prec b and b set%prec c)
            implies 
          a set%prec c)"
    (theory generic-theory-1)
    (proof
      (
        
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%subseteq-transitivity)
        auto-instantiate-existential
        )))

(def-theorem ()
    "forall(a:sets[ind_1],a set%prec a)"
    (theory generic-theory-1)
    (proof
      (
        (unfold-single-defined-constant (0) set%prec)
        )))

(def-theorem ()
    "forall(a,b:sets[ind_1],
                      a set%prec b and b set%prec a implies a=b)"
    (theory generic-theory-1)
    (proof
      (
      unfold-defined-constants
      (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
      )))

(def-theorem ()
    "forall(p:[sets[ind_1],prop],
          nonvacuous_q{p}
            and 
          forsome(alpha:sets[ind_1],
              forall(theta:sets[ind_1],
                  p(theta) implies theta set%prec alpha))
            implies 
          forsome(gamma:sets[ind_1],
              forall(theta:sets[ind_1],
                  p(theta) implies theta set%prec gamma)
                and 
              forall(gamma_1:sets[ind_1],
                  forall(theta:sets[ind_1],
                      p(theta) implies theta set%prec gamma_1)
                    implies 
            gamma set%prec gamma_1)))"
    (theory generic-theory-1)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("indic{x:ind_1, forsome(b:sets[ind_1], p(b) and x in b)}"))
        simplify-insistently
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        simplify-insistently
        )))

(def-translation complete-partial-order-to-generic-theory-1 
    (source complete-partial-order)
    (target generic-theory-1)
    (fixed-theories h-o-real-arithmetic)
    (constant-pairs
      (prec set%prec))
    (sort-pairs (uu "sets[ind_1]"))
    (theory-interpretation-check using-simplification))

(def-transported-symbols monotone
    (translation complete-partial-order-to-generic-theory-1)
    (renamer cpo-gt-renamer)
    )
        

(def-overloading monotone
    (complete-partial-order monotone)
    (generic-theory-1  gt%monotone))

(def-theorem monotonicity-of-sb-functional 
    "forall(f:[ind_2,ind_1],g:[ind_1,ind_2],
                        monotone(lambda(x:sets[ind_1],image(f,image(g,x)^^)^^)))"
    (theory generic-theory-2)
    lemma
    (proof
      (
        (unfold-single-defined-constant-globally gt%monotone)
        (unfold-single-defined-constant-globally set%prec)
        simplify-insistently
        (prove-by-logic-and-simplification 3)
        )))