(def-language graph-language
    (embedded-language the-kernel-theory)
    (base-types vertices edges)
    (constants
      (endpoints "[edges -> sets[vertices]]")))

(def-theory graphs 
    (language graph-language)
    (component-theories h-o-real-arithmetic)
    (axioms
      (edges-have-two-endpoints
        "forall(e:edges, forsome(v_1,v_2: vertices,
              endpoints(e) = singleton{v_1} union singleton{v_2}))")))

(def-theorem endpoints-is-total 
    "total_q{endpoints,[edges -> sets[vertices]]}"
    (usages d-r-convergence)
    (theory graphs)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem edges-have-two-endpoints ("x_0"))
        )))

(def-constant loop 
    "lambda(e:edges, singleton{endpoints(e)})"
    (theory graphs))

(def-constant parallel 
    "lambda(e_1,e_2:edges, endpoints(e_1) = endpoints(e_2))"
    (theory graphs))

(def-constant adjacent%vertices 
    "lambda(v_1,v_2:vertices, forsome(e:edges, 
          endpoints(e) = singleton{v_1} union singleton{v_2}))"
    (theory graphs))

(def-constant adjacent%edges 
    "lambda(e_1,e_2:edges, forsome(v:vertices,
          v in endpoints(e_1)  and v in endpoints(e_2)))"
    (theory graphs))

(def-constant vertex%incidence%set 
    "lambda(v:vertices, indic{e:edges, v in endpoints(e)})"
    (theory graphs))

(def-constant degree 
    "lambda(v:vertices, f_card{vertex%incidence%set(v)})"
    (theory graphs))

(def-constant isolated 
    "lambda(v:vertices, degree(v) = 0)"
    (theory graphs))