--BEGIN HERE
--
-- \section{Introductory note}
--
-- This scenario undertakes the study of connectivity, treated here as a property
-- of hypergraphs. Hypergraphs are defined to be just finite sets of edges,
-- each edge being, in its turn, a finite set of cardinality two or more.
-- The elements of the edges of a hypergraph are called its vertices, or nodes
-- (deliberately, we are leaving out of our study hypergraphs with isolated nodes). 
--
-- Ordinary graphs simply are, from this perspective, finite sets of doubletons.
--
-- A hypergraph $G$ is said to be connected when it has no subset $P$,
-- other than $0$ and $G$ itself, such that $P$ and $G-P$ share no nodes.
-- Trivial examples of connected hypergraphs are: $0$; every singleton
-- ${e}$ whose element $e$ is finite, non-null, and non-singleton;
-- every doubleton hypergraph ${e0,e1}$ with $e0*e1/=0$.
--
-- We will prove that one can always remove one of the nodes
-- of a connected non-null hypergraph without disrupting its connectivity;
-- but, preliminary to showing that, we must explain how nodes get removed.
-- Removing a node $w$ from an ordinary graph $G$ amounts to withdrawing
-- from $G$ all edges to which $w$ belongs; but when $G$ is a hypergraph
-- endowed with at least one non-doubleton edge, node removal becomes
-- a more complicated operation. Speaking in general, removing a node $w$
-- will amount to withdrawing all doubleton edges to which $w$ belongs,
-- at the same time deleting $w$ from every other edge (the edges to which
-- $w$ does not belong are nohow affected by the removal operation).
--
-- Now we are ready to define a cut vertex of an hypergraph $G$ (typically connected)
-- as being a node $w$ such that $G$  does not have the form $G={{u,w}}$,
-- and either a disconnectd graph results from the removal of $w$ from $G$,
-- or some node different from $w$ gets lost in consequence of the removal of $w$.
-- Our target theorem hence is that every non-null graph $G$ has a node which is
-- not a cut vertex of $G$.
--
-- Henceforth hypergraphs will be simply called graphs, for brevity.
--
-- The proofs carried out in this scenario follow rather closely the guidelines
-- of the conference paper
-- [CO14] A. Casagrande, E. G. Omodeo:
--        Reasoning about Connectivity without Paths, ICTCS 2014, Perugia.
-- The propositions in that paper are identified by the names: Lemmas 1,...,21,
-- Theorems 1 and 2, and Corollary 1; a reference to each of them is provided near 
-- the corresponding Theorem hgraphXXX within this scenario. The only missing
-- proposition here is Theorem 1, whose proof has been embedded in the proof
-- of Corollary 1 (Theorem hgraph24 in this document); on the other hand, a few
-- (relatively marginal) propositions not proved in that paper will enter
-- into play more visibly here. 
--
-- \section{Prerequisites}
--
-- \subsection{Basic laws on the power-set and sum-set global operations}
--
Def pow: [Family of all subsets of a given set] pow(S) := { x : x 可ncin S }
--
--
-- Our next theorem characterizes the powerset formation operation in
-- more usable terms than the very definition of this construct. It also
-- proves that no set can equal is own powerset (else it should belong to itself,
-- against the acyclicity of membership).
--
Theorem pow_0: [Characterization of powerset; also: no set equals its own powerset] ((X incs Y) 占q (Y in pow(X))) & (X /= pow(X)). Proof:
Suppose_not(x0,y0) ==> AUTO
--
-- We begin by excluding the possibility that $x0 = pow(x0)$:
--
	Suppose ==> Stat0: x0 notin {y: y 可ncin x0}
	x0-->Stat0 ==> false; Discharge ==> AUTO 
	Use_def(pow(x0)) ==> AUTO
--
-- Arguing by contradiction, if $x0,y0$ constituted a counterexample,
-- then either one of the literals $x0 incs y0$ and $y0 in {y: y 可ncin x0}$
-- would be true and the other one would be false.
--
	EQUAL ==> Stat1: (x0 incs y0) 叩eq (y0 in {y: y 可ncin x0})
--
-- If it is the second that is true then, via a substitution in the setformer,
-- we would contradict the falsity of the first.
--
	Suppose ==> Stat2: y0 in {y: y 可ncin x0}
	y1-->Stat2(Stat1*) ==> false; Discharge ==> Stat3: y0 notin {y: y 可ncin x0}
--
-- But then the literals $x0 incs y0$ and $y0 notin {y: y 可ncin x0}$ should hold together,
-- which gives us a contradiction if we replace the bounded variable $y$ of the setformer
-- by $y0$.  
--
	y0-->Stat3(Stat1*) ==>false
	Discharge ==> QED
--
Theorem pow_1: [Monotonicity of powerset] (S incs X) 可mp ((pow(X) + {0,X}) 可ncin pow(S)). Proof:
Suppose_not(s0,x0) ==> AUTO
    Set_monot ==> { x : x 可ncin x0 } 可ncin { x : x 可ncin s0 }
    Use_def(pow) ==> Stat1: (0 notin { x : x 可ncin s0 }) or (x0 notin { x : x 可ncin s0 })
    (0,x0)-->Stat1 ==> false
    Discharge ==> QED
--
Theorem pow_2: [Powerset of null set and of singletons] (pow(0) = {0}) & (pow({X}) = {0,{X}}). Proof:
Suppose_not(x0) ==> AUTO
    Suppose ==> pow(0) /= {0}
        (0,0)-->Tpow_1 ==> Stat0: pow(0) 叩incin {0}
        y0-->Stat0(Stat0*) ==> Stat1: (y0 in pow(0)) & (y0 notin {0})
        (0,y0)-->Tpow_0(Stat1*) ==> false
    Discharge ==> (pow({x0}) /= {0,{x0}})
    ({x0},{x0})-->Tpow_1 ==> Stat2: pow({x0}) 叩incin {0,{x0}}
    y1-->Stat2 ==> Stat3: (y1 in pow({x0})) & (y1 notin {0,{x0}})
    ({x0},y1)-->Tpow_0(Stat3*) ==> false
    Discharge ==> QED
--
Def unionset: [Family of all members of members of a set] Un(S) := {u: v in S, u in v}
--
Theorem un_0: [Unionset operation yielding null result] (Un(X) = 0) 占q (X 可ncin {0}). Proof:
Suppose_not(x0) ==> AUTO
    Use_def(Un(x0)) ==> AUTO
    Suppose ==> Stat1: (x0 叩incin {0}) & ({y: x in x0, y in x} = 0)
    (x1,x1,arb(x1))-->Stat1(Stat1) ==> false; Discharge ==> Stat2: ({y: x in x0, y in x} /= 0) & (x0 可ncin {0})
    (x2,y2)-->Stat2(Stat2*) ==> false
    Discharge ==> QED
--
--
Theorem un_2: [Unionset operation combined with set adjunction] (X + {Y} = Z) 可mp (Un(Z) = Un(X) + Y). Proof:
Suppose_not(x0,y0,z0) ==> AUTO
    EQUAL ==> Stat0: Un(x0 + {y0}) /= Un(x0) + y0
    Use_def(Un)(Stat0) ==> Stat1: {y: x in x0+{y0}, y in x} /= ({yp: xp in x0, yp in xp} + y0)
    c-->Stat1(Stat1*) ==> (c in {y: x in x0+{y0}, y in x}) 叩eq (c in ({yp: xp in x0, yp in xp} + y0))
    Suppose ==> Stat2: (c in {y: x in x0+{y0}, y in x}) & (c notin {yp: xp in x0, yp in xp}) & (c notin y0)
    (x1,y1,x1,y1)-->Stat2(Stat2*) ==> false; Discharge ==> AUTO
    Suppose ==> Stat3: (c notin {y: x in x0+{y0}, y in x}) & (c in y0)
    (y0,c)-->Stat3(Stat3*) ==> false; Discharge ==> Stat4: (c in {yp: xp in x0, yp in xp}) & (c notin {y: x in x0+{y0}, y in x})
    (x2,y2,x2,y2)-->Stat4(Stat4*) ==> false
    Discharge ==> QED
--
--
Theorem un_4: [Unionset operation applied to a singleton] ({Y} = Z) 可mp (Un(Z) = Y). Proof:
Suppose_not(y0,z0) ==> AUTO
    0-->Tun_0(*) ==> Un(0) = 0
    (0,y0,z0)-->Tun_2(*) ==> false
    Discharge ==> QED
--
--
-- \subsection{Basic laws on the finiteness property, and associated `THEORY's}
--
--
--
-- Traditionally, finiteness is defined through the notion of cardinality of a set:
-- a set is finite if its cardinality precedes the first infinite ordinal. As a shortcut, to begin
-- developing an acceptable formal treatment of finiteness without much preparatory work, we adopt
-- here the following definition (reminiscent of Tarski's 1924 paper "Sur les ensembles fini"):
-- a set $F$ is \emph{finite} if every non-null family of subsets of $F$ owns an inclusion-minimal element.
-- This notion can be specified very succinctly in terms of the powerset operator. 
--
--
Def Fin: [Finiteness property] Finite(F) := (FORALL g in (pow(pow(F)) - {0}) | (EXISTS m | (g * pow(m)) = {m}))
--
Theorem fin_0: [Monotonicity of finiteness] ((Y incs X) & Finite(Y)) 可mp Finite(X). Proof:
Suppose_not(y0,x0) ==> AUTO
    (y0,x0)-->Tpow_1(*) ==> pow(y0) incs pow(x0)
    Use_def(Finite) ==> Stat1: (not(FORALL g in (pow(pow(x0)) - {0}) | (EXISTS m | (g * pow(m)) = {m}))) & (FORALL gp in (pow(pow(y0)) - {0}) | (EXISTS m | (gp * pow(m)) = {m}))
    (pow(y0),pow(x0))-->Tpow_1(*) ==> pow(pow(y0)) incs pow(pow(x0))
    (g0,g0)-->Stat1(Stat1*) ==> (not(EXISTS m | (g0 * pow(m)) = {m})) & (EXISTS m | (g0 * pow(m)) = {m})
    Discharge ==> QED
--
--
Theorem fin_1: [Finiteness of the union of a finite set with a singleton] Finite(F) 可mp Finite(F + {X}). Proof:
Suppose_not(f0,x0) ==> AUTO
--
-- Arguing by contradiction, suppose that $f0$ and $x0$ are such that $f0$ is finite but $f0 + {x0}$ is not.
-- A nonnull familiy $g0$ of subsets of $f0 +{x0}$ must then exist none of whose elements is minimal.
-- On the other hand ${y-{x0}: y in g0}$, which is also nonnull but consists entirely of subsets of $f0$,
-- must have a minimal element $m0=y0-{x0}$, with $y0 in g0$. 
--
    Use_def(Finite) ==> Stat0: (not(FORALL g in (pow(pow(f0+{x0})) - {0}) | (EXISTS m | (g * pow(m)) = {m}))) & Stat1: (FORALL h in (pow(pow(f0)) - {0}) | (EXISTS m | (h * pow(m)) = {m}))
    g0-->Stat0(Stat0) ==> Stat2: (not (EXISTS m | (g0 * pow(m)) = {m})) & (g0 in pow(pow(f0+{x0}))) & (g0 /= 0)
    Loc_def ==> Stat3: h0 = {y-{x0}: y in g0}
    Suppose ==> h0 notin (pow(pow(f0)) - {0})
        Suppose ==> Stat4: {y-{x0}: y in g0} = 0
        (arb(g0))-->Stat4(Stat2,Stat2)  ==> false; Discharge ==> AUTO
        Use_def(pow) ==> Stat5: h0 notin {h: h 可ncin {k: k 可ncin f0}}
        h0-->Stat5(Stat5*) ==> Stat6: h0 叩incin {k: k 可ncin f0}
        k0-->Stat6(Stat3*) ==> Stat7: (k0 in {y-{x0}: y in g0}) & (k0 notin {k: k 可ncin f0})
        (y1,k0)-->Stat7(Stat7*) ==> (y1 in g0) & (y1 叩incin (f0 + {x0}))
        Use_def(pow)(Stat2,Stat2) ==> Stat8: g0 in {h: h 可ncin {k: k 可ncin (f0 + {x0})}}
        h1-->Stat8(Stat7*) ==> Stat9: y1 in {k: k 可ncin (f0 + {x0})}
        k1-->Stat9(Stat7*) ==> false
    Discharge ==> AUTO
    (h0,m0)-->Stat1(Stat3*) ==> Stat10: (m0 in {y-{x0}: y in g0}) & ((h0 * pow(m0)) = {m0})
    y0-->Stat10(Stat10*) ==> Stat11: (m0 = (y0-{x0})) & (y0 in g0)
--
-- We will reach the desired contradiction by showing that either $m0$ or $y0=m0+{x0}$ is minimal in $g0$.
-- We check first that $m0$ itself must be minimal when $m0 in g0$.
--
    Suppose ==> m0 in g0
        m0-->Stat2(Stat10*) ==> Stat12: (g0 * pow(m0)) 叩incin {m0}
        Use_def(pow(m0)) ==> AUTO
        z0-->Stat12(Stat3*) ==> Stat13: (z0 in {h: h 可ncin m0}) & (z0 notin {y-{x0}: y in g0}) & (z0 in g0)
        (h2,z0)-->Stat13(Stat11*) ==> false
    Discharge ==> AUTO
--
-- Suppose next that $m0 notin g0$; we will reach a contradiction by showing that $y0$ is minimal in $g0$.
--
    Suppose ==> y0 notin pow(y0)
        Use_def(pow) ==> Stat13a: y0 notin {s: s 可ncin y0}
        y0-->Stat13a(Stat13a*) ==> false
    Discharge ==> AUTO 
    y0-->Stat2(Stat11*) ==> Stat14: (g0 * pow(y0)) 叩incin {y0}
    Use_def(pow(y0)) ==> AUTO    
    z1-->Stat14(Stat11*) ==> Stat15: (z1 in {h: h 可ncin y0}) & (z1 in g0) & ((z1-{x0}) /= (y0-{x0}))
    EQUAL(Stat10) ==> (h0 * pow(y0-{x0})) = {y0-{x0}}
    Suppose ==> (z1-{x0}) notin pow(y0-{x0})
        Use_def(pow)(Stat15) ==> Stat16: (z1-{x0}) notin {h: h 可ncin (y0-{x0})}
        (z1-{x0})-->Stat16(Stat16*) ==> (z1-{x0}) 叩incin (y0-{x0})
        h3-->Stat15(Stat16*) ==> false
    Discharge ==> AUTO
    Suppose ==> Stat17: (z1-{x0}) notin {y-{x0}: y in g0}
    z1-->Stat17(Stat15*) ==> false; Discharge ==> (z1-{x0}) in h0
    (Stat15*)Discharge ==> QED
--
--
Theorem fin_2: [Singletons are finite] Finite({X}) & Finite(0). Proof:
Suppose_not(x0) ==> AUTO
    ({x0},0)-->Tfin_0 ==> not Finite({x0})
    Use_def(Finite) ==> Stat1: (not(FORALL g in (pow(pow({x0})) - {0}) | (EXISTS m | (g * pow(m)) = {m})))
    g0-->Stat1 ==> Stat2: (not (EXISTS m | (g0 * pow(m)) = {m})) &  (g0 in (pow(pow({x0})) - {0}))
    Use_def(pow) ==>  Stat3: g0 in {y: y 可ncin pow({x0})}
    x0-->Tpow_2 ==> AUTO
    y0-->Stat3(Stat2*) ==> Stat4: (g0 /= 0) & (g0 可ncin {0,{x0}})
    Suppose ==> 0 in g0
        0-->Stat2(Stat3*) ==> false
    Discharge ==> g0 = {{x0}}
    ({x0})-->Stat2(Stat3*) ==> false
    Discharge ==> QED
--
--
THEORY finiteInduction(s0, P(S))
    Finite(s0) & P(s0)
END finiteInduction
--
ENTER_THEORY finiteInduction
--
Theorem finiteInduction0: (EXISTS m | ({s 可ncin s0 | P(s)} * pow(m)) = {m}). Proof:
Suppose_not() ==> AUTO
    Assump ==> Finite(s0) & P(s0)
    Use_def(Finite) ==> Stat1: (FORALL g in (pow(pow(s0)) - {0}) | (EXISTS m | (g * pow(m)) = {m}))
    ({s 可ncin s0 | P(s)})-->Stat1 ==> {s 可ncin s0 | P(s)} notin (pow(pow(s0)) - {0})
    Suppose ==> Stat2: s0 notin {s 可ncin s0 | P(s)}
    s0-->Stat2 ==> false; Discharge ==> {s 可ncin s0 | P(s)} notin (pow(pow(s0)))
    Use_def(pow) ==> Stat3: {s 可ncin s0 | P(s)} notin {y: y 可ncin {z: z 可ncin s0}}
    ({s 可ncin s0 | P(s)})-->Stat3 ==> Stat4: {s 可ncin s0 | P(s)} 叩incin {z: z 可ncin s0}
    s1-->Stat4 ==> Stat5: (s1 in {s: s 可ncin s0 | P(s)}) & (s1 notin {z: z 可ncin s0})
    (s,s1)-->Stat5(Stat5*) ==> false
    Discharge ==> QED
--
APPLY(v1_thryvar:fin_thryvar) Skolem() ==> 
    Theorem finiteInduction1: ({s 可ncin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar}
--
Theorem finiteInduction2: [Minimal finite set satisfying $P$] (S 可ncin fin_thryvar) 可mp( Finite(S) & ( P(S) 占q (S = fin_thryvar)) ). Proof:
Suppose_not(s1) ==> AUTO
    ()-->TfiniteInduction1 ==> (({s 可ncin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar}) & Stat1: (fin_thryvar in {s 可ncin s0 | P(s)})
    ()-->Stat1 ==> (fin_thryvar 可ncin s0) & P(fin_thryvar)
    Assump ==> Finite(s0)
    (s0,fin_thryvar)-->Tfin_0 ==> Finite(fin_thryvar)
    (fin_thryvar,s1)-->Tfin_0 ==> P(s1) 叩eq (s1 = fin_thryvar)
    Suppose ==> s1 = fin_thryvar
    EQUAL ==> false; Discharge ==> (s1 notin ({s 可ncin s0 | P(s)} * pow(fin_thryvar))) & P(s1) 
    Suppose ==> s1 notin pow(fin_thryvar)
        Use_def(pow) ==> Stat2: s1 notin {y: y  可ncin fin_thryvar}
        s1--> Stat2 ==> false
    Discharge ==> Stat3: s1 notin {s 可ncin s0 | P(s)}
    s1-->Stat3 ==> false
    Discharge ==> QED
--
ENTER_THEORY Set_theory
--
--DISPLAY finiteInduction
--
--THEORY finiteInduction(s0,P(S))
--    Finite(s0) & P(s0)
--==>(fin_thryvar)
--    (FORALL S | (S 可ncin fin_thryvar) 可mp ( Finite(S) & ( P(S) 占q (S = fin_thryvar)) ))
--END finiteInduction
--
Theorem fin_3: [Finiteness of the union of two finites sets] (Finite(X) & Finite(Y)) 可mp Finite(X+Y). Proof:
Suppose_not(x0,y1) ==> AUTO
--
-- Arguing by contradiction, suppose that $x0$ and $y1$ are finite sets whose union is not finite.
-- The finite induction enables us to take a minimal subset $y0$ of $y1$ for which $x0+y0$ is not finite.
--
    APPLY(fin_thryvar:y0) finiteInduction(s0->y1,P(S)->(not Finite(x0+S))) ==>
        Stat1: (FORALL s | (s 可ncin y0) 可mp ( Finite(s) & ( (not Finite(x0+s)) 占q (s = y0)) ))
        y0-->Stat1(Stat1*) ==> Finite(y0) & (not Finite(x0+y0))
        Loc_def ==> a0 = arb(y0)
--
-- Since $y0$ cannot be empty, the union $x0+y0$ can be decomposed as $x0+(y0-{arb(y0)})+{arb(y0)}$,
-- where $x0+(y0-{arb(y0)})$ is finite by inductive hypothesis. But then $x0+y0$ must also be finite
-- by Theorem fin_1
--
    Suppose ==> x0+y0=x0
    EQUAL ==> false; Discharge ==>  Stat2: y0-{a0} /= y0
    (y0-{a0})-->Stat1(Stat1*) ==> Finite(x0+(y0-{a0}))
    (x0+(y0-{a0}),a0)-->Tfin_1(Stat2*) ==> Finite(x0+(y0-{a0})+{a0})
    EQUAL(Stat1) ==> false
    Discharge ==> QED
--
--
--
Theorem fin_4: [Every nonnull finite set has an inclusion-maximal element] (Finite(S) & (S /= 0)) 可mp (EXISTS m in S | {x in S-{m} | m 可ncin x} = 0). Proof:
Suppose_not(s1) ==> AUTO
--
-- To start an inductive argument by contradiction, suppose $s2$ is an inclusion-minimal counterexample.
--
    APPLY(fin_thryvar:s2) finiteInduction(s0->s1,P(S)->((S /= 0) & (not (EXISTS m in S | {x in S-{m} | m 可ncin x} = 0)))) ==>
        Stat1: (FORALL s | (s 可ncin s2) 可mp ( Finite(s) & ( ((s /= 0) & (not (EXISTS m in S | {x in S-{m} | m 可ncin x} = 0))) 占q (s = s2)) ))
    s2-->Stat1(Stat1*) ==> Stat2: (s2 /= 0) & Stat3: (not (EXISTS m in s2 | {x in s2-{m} | m 可ncin x} = 0)) 
--
-- Draw from this set $s2$, where no element is maximal, an element $x2$.
-- Since $x2$ is not maximal, there is an $x3 in s2$ exceeding it. 
--
    (x2,x2)-->Stat2(Stat2*) ==> Stat4: ({x in s2-{x2} | x2 可ncin x} /= 0) & (x2 in s2)
    x3-->Stat4(Stat4*) ==> (x3 in s2-{x2}) & (x2 可ncin x3)
--
-- Due to the minimality assumption concerning $s2$, there is a maximal element $m0$ in $s2-{x2}$. 
--
    (s2-{x2})-->Stat1(Stat4*) ==> Stat5: (EXISTS m in s2-{x2} | {x in s2-{x2}-{m} | m 可ncin x} = 0)
    m0-->Stat5(Stat5*) ==> Stat6: ({x in s2-{x2}-{m0} | m0 可ncin x} = 0) & (m0 in s2-{x2})
--
-- This $m0$ is not maximal in $s2$; therefore, unlike $x3$, it must be included in $x2$.
--
    m0-->Stat3(Stat6*) ==> Stat7: ({x in s2-{m0} | m0 可ncin x} /= 0) & ({x in s2-{x2}-{m0} | m0 可ncin x} = 0) 
    (x4,x4)-->Stat7(Stat7*) ==> m0 可ncin x2
--
-- But then $x3$ exceeds $m0$, which contradicts the maximality of $m0$ in $s2-{x2}$.
--
    x3-->Stat6(Stat4*) ==> false
    Discharge ==> QED   

--
--
THEORY finiteImage(s0,f(X))
    Finite(s0)
END finiteImage
--
ENTER_THEORY finiteImage
--
Theorem finiteImage: Finite({f(x): x in s0}). Proof:
Suppose_not() ==> AUTO
--
-- We can prove the claim by means of finite induction. Arguing by contradiction, let us
-- assume that $s0$ has, via the global function $f(X)$, infinite image; then take an $s1$
-- which is finite and minimal (w.r.t. inclusion) and has, much like $s0$, infinite image
-- ${f(x): x in s1}$.  As one sees easily, $s1 /= 0$; hence, if we remove an element $a$
-- from $s1$, we find that ${f(x): x in (s1 - {a})}$ is finite in consequence of the
-- supposed minimality of $s1$. Since the union of two finite sets is finite,
-- we get the finiteness of ${f(x): x in (s1 - {a})} + {f(a)}$,
-- which hence must differ from ${f(x): x in s1}$.
--
    Assump ==> Finite(s0)
    APPLY(fin_thryvar:s1) finiteInduction(s0->s0,P(S)->(not Finite({f(x): x in S}))) ==>
	Stat1: (FORALL s | (s 可ncin s1) 可mp ( Finite(s) & ((not Finite({f(x): x in s})) 占q (s = s1)) ))
    s1-->Stat1 ==> not Finite({f(x): x in s1})
    Loc_def ==> Stat0: a = arb(s1)
    (f(a))-->Tfin_2 ==> Finite({f(a)}) & Finite(0)    
    Suppose ==> s1 = 0
        ELEM ==> {f(x): x in 0} = 0
        EQUAL ==> false
    Discharge ==> AUTO
    (Stat0)ELEM ==> Stat2: ((s1 - {a}) 可ncin s1) & ((s1 - {a}) /= s1)
    Suppose ==> {f(x): x in s1} = ({f(x): x in (s1 - {a})} + {f(a)})
        (s1 - {a})-->Stat1(Stat2*) ==> Finite({f(x): x in (s1 - {a})})
        ({f(x): x in (s1 - {a})},f(a))-->Tfin_1(Stat1*) ==> Finite({f(x): x in (s1 - {a})} + {f(a)})
        EQUAL(Stat1) ==> false
    Discharge ==> AUTO
--
-- On the other hand, ${f(x): x in (s1 - {a})} + {f(a)}$ and ${f(x): x in s1}$ must be equal:
-- in fact $a in s1$, and therefore $f(a) in {f(x): x in s1}$; moreover, by monotonicity,
-- ${f(x): x in (s1 - {a})} 可ncin {f(x): x in s1}$ and...
--
    Set_monot ==> {f(x): x in (s1 - {a})} 可ncin {f(x): x in s1}
    Suppose ==> Stat3: f(a) notin {f(x): x in s1}
    a-->Stat3(Stat2,Stat2*) ==> false; Discharge ==> Stat4: {f(x): x in s1} 叩incin ({f(x): x in (s1 - {a})} + {f(a)})
--
-- ...one easily sees that ${f(x): x in s1} 可ncin ({f(x): x in (s1 - {a})} + {f(a)})$, ...
--
    b-->Stat4(Stat4*) ==> Stat5: (b in {f(x): x in s1}) & (b notin ({f(x): x in (s1 - {a})} + {f(a)}))
    x0-->Stat5(Stat5*) ==> (f(x0) notin {f(x): x in (s1 - {a})}) & (x0 in s1) & (f(x0) /= f(a))
    Suppose ==> x0 = a
    EQUAL(Stat5) ==> false; Discharge ==> Stat6: (f(x0) notin {f(x): x in (s1 - {a})}) & (x0 /= a) & (x0 in s1)
    x0-->Stat6(Stat6*)==> false
--
-- which leads us to the sought contradiction.
--
    Discharge ==> QED
--
--
ENTER_THEORY Set_theory	
--
-- DISPLAY finiteImage
--
-- THEORY finiteImage(s0,f(X))
--	Finite(s0)
-- ==>
--	Finite({f(x): x in s0})
-- END finiteImage
--
Theorem fin_5: [Powersets of finite sets are finite] Finite(F) 可mp Finite(pow(F)). Proof:
Suppose_not(f1) ==> AUTO
--
-- We can prove the claim by means of finite induction. Arguing by contradiction, let us
-- assume that $f1$ is finite but has an infinite powerset; then take an $f0$
-- which is finite and minimal (w.r.t. inclusion) and has, much like $f1$, infinite powerset.
-- As one sees easily, $f0 /= 0$; hence, if we remove an element $a$
-- from $f0$, we find that $pow(f0 - {a})$ is finite in consequence of the
-- supposed minimality of $f0$.
--
    APPLY(fin_thryvar:f0) finiteInduction(s0->f1,P(S)->(not Finite(pow(S)))) ==>
	Stat1: (FORALL s | (s 可ncin f0) 可mp ( Finite(s) & ((not Finite(pow(s))) 占q (s = f0)) ))
    f0-->Stat1 ==> not Finite(pow(f0))
    Suppose ==> f0 = 0
        0-->Tfin_2(Stat1*) ==> Finite({0})
        Suppose ==> pow(0) = {0}
        EQUAL ==> false; Discharge ==> AUTO
        Use_def(pow(0)) ==> AUTO
        (0,0)-->Tpow_1(Stat1*) ==> Stat2: {x: x 可ncin 0} 叩incin {0}
        x0-->Stat2(Stat2*) ==> Stat3: (x0 in {x: x 可ncin 0}) & (x0 /= 0)
        x1-->Stat3(Stat3*) ==> false
    Discharge ==> Stat4: f0 /= 0
    a-->Stat4(Stat4*) ==> a in f0
    (f0-{a})-->Stat1(Stat4*) ==> Finite(pow(f0-{a}))
--
--
--
    (f0,f0-{a})-->Tpow_1(Stat4*) ==> pow(f0) = pow(f0-{a}) + (pow(f0)-pow(f0-{a}))
    EQUAL(Stat1) ==> not Finite(pow(f0-{a}) + (pow(f0)-pow(f0-{a})))
    (pow(f0-{a}),pow(f0)-pow(f0-{a}))-->Tfin_3(Stat1*) ==> not Finite(pow(f0)-pow(f0-{a}))
    Suppose ==> Stat5: pow(f0)-pow(f0-{a}) /= {x+{a}: x in pow(f0-{a})}
        b-->Stat5 ==> AUTO
        Use_def(pow(f0)) ==> AUTO
        Use_def(pow(f0-{a})) ==> AUTO
        Suppose ==> Stat6: b in {x+{a}: x in pow(f0-{a})}
            x2-->Stat6(Stat5*) ==> Stat7: (x2 in {y: y 可ncin (f0-{a})}) & (b=x2+{a})
            y2-->Stat7(Stat7*) ==> x2 可ncin (f0-{a})
            (Stat5*)ELEM ==> Stat8: (b in {y: y 可ncin (f0-{a})}) or (b notin {y: y 可ncin f0})
            (y1,b)-->Stat8(Stat4*) ==> false
        Discharge ==> AUTO
        (Stat5*)ELEM ==> Stat9: (b in {y: y 可ncin f0}) & (b notin {y: y 可ncin (f0-{a})}) & (b notin {x+{a}: x in pow(f0-{a})})
        (y0,y0,y0-{a})-->Stat9(Stat5*) ==> Stat10: (y0-{a} notin {y: y 可ncin (f0-{a})}) & (y0 可ncin f0) & (a in y0)
        (y0-{a})-->Stat10(Stat10*) ==> false
    Discharge ==> AUTO
    APPLY() finiteImage(s0->(pow(f0-{a})),f(X)->(x+{a})) ==> Finite({x+{a}: x in pow(f0-{a})})
    EQUAL ==> false; Discharge ==> QED
--
--
Theorem fin_6: [Sets whose sum-set is finite are finite] Finite(Un(F)) 可mp Finite(F). Proof:
Suppose_not(f0) ==> AUTO
    Suppose ==> f0 可ncin pow(Un(f0))
        (pow(Un(f0)),f0)-->Tfin_0(*) ==> not Finite(pow(Un(f0)))
        (Un(f0))-->Tfin_5(*) ==> false
    Discharge ==> Stat1: f0 叩incin pow(Un(f0))
    Use_def(pow(Un(f0))) ==> AUTO
    x0-->Stat1(Stat1*) ==> Stat2: (x0 notin {y: y 可ncin Un(f0)}) & (x0 in f0)
    x0-->Stat2(Stat2*) ==> (x0 叩incin Un(f0)) & (x0 in f0)
    (f0,x0,f0)-->Tun_2(*) ==> false
    Discharge ==> QED
--
-- \section{Connected hypergraphs have non-cut vertices}
--
-- \subsection{Sum-set will conveniently represent the operation supplying the set of nodes underlying a hypergraph}
--
Def roughCard2: [Having two or more elements] CardAtLeast2(E) := E 叩incin {arb(E)}
--
Def hgraph0: ['nodes' is an alias of sum-set] nodes(G) := Un(G)
--
Def hgraph1: [An edge to which a given vertex belongs] edgeOf(V,G) := arb({e in G | V in e})
--
-- The following proposition corresponds to Lemma 9 of [CO14].
--
Theorem hgraph_a: [Sumset monotonicity] (P 可ncin G) 可mp (nodes(P) 可ncin nodes(G)). Proof:
Suppose_not(p0,g0) ==> AUTO
    Use_def(Un) ==> (Un(p0) = {v: e in p0, v in e}) & (Un(g0) = {v: e in g0, v in e}) 
    Set_monot ==> {v: e in p0, v in e} 可ncin {v: e in g0, v in e}
    Use_def(nodes) ==> false 
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 10 of [CO14].
--
Theorem hgraph_b: [Sumset distributes over dyadic union] nodes(P+Q) = nodes(P) + nodes(Q). Proof:
Suppose_not(p0,q0) ==> AUTO
    (p0,p0+q0)-->Thgraph_a ==> AUTO
    (q0,p0+q0)-->Thgraph_a ==> Stat1: nodes(p0+q0) 叩incin (nodes(p0) + nodes(q0))
    v0-->Stat1(Stat1*) ==> (v0 in nodes(p0+q0)) & (v0 notin  (nodes(p0) + nodes(q0)))
    Use_def(nodes) ==> (v0 in Un(p0+q0)) & (v0 notin (Un(p0) + Un(q0)))
    Use_def(Un) ==> Stat2: (v0 in {v: e in p0+q0, v in e}) & (v0 notin {v: e in p0, v in e}) & (v0 notin {v: e in q0, v in e})
    (e1,v1,e1,v0,e1,v0)-->Stat2(Stat2*) ==> false
    Discharge ==> QED
--
--
-- The following proposition corresponds to Lemma 11 of [CO14].
--
Theorem hgraph_c: [Sumset disjointness law for two sets of which one includes the other] (P 可ncin G) 可mp ((nodes(P) * nodes(G-P) = 0) 占q (FORALL e in G | 0 in {nodes(P)*e,nodes(G-P)*e})). Proof:
Suppose_not(p0,g0) ==> AUTO
    Use_def(nodes) ==> Stat1: (p0 可ncin g0) & ((Un(p0) * Un(g0-p0) = 0) 叩eq (FORALL e in g0 | 0 in {Un(p0)*e,Un(g0-p0)*e}))
--
-- Arguing by contradiction, suppose that $p0,g0$ form a counterexample.
-- Recall that 'nodes' simply is an alias for the sum-set operator.
-- Thus either (1) $Un(p0) * Un(g0-p0) = 0$ and $not(FORALL e in g0 | 0 in {Un(p0)*e,Un(g0-p0)*e})$ hold together;
-- or (2) $Un(p0) * Un(g0-p0) /= 0$ and $(FORALL e in g0 | 0 in {Un(p0)*e,Un(g0-p0)*e})$ hold together.
-- We will exclude both possibilities, arguing as follows.
--
    Suppose ==> Stat3: not(FORALL e in g0 | 0 in {Un(p0)*e,Un(g0-p0)*e})
--
-- Possibility (1) leads to a contradiction: in fact, if $e0 in g0$ is such that
-- $Un(p0)*e0$ and $Un(g0-p0)*e0$ are non-null, then either $e0 in p0$ or $e0 in g0-p0$ must hold,
-- but in the former case $e0 可ncin Un(p0)$ and hence $Un(p0)$ and $Un(g0-p0)$ would intersect;
-- likewise, in the latter case $e0 可ncin Un(g0-p0)$ and hence $Un(p0)$ and $Un(g0-p0)$ intersect again.
--
        e0-->Stat3(Stat1*) ==> Stat4: (0 /= Un(p0)*e0) & (0 /= Un(g0-p0)*e0) & (Un(p0) * Un(g0-p0) = 0) & (e0 in g0)
        Suppose ==> e0 in p0
            (p0,e0,p0)-->Tun_2(Stat4*) ==> false
        Discharge ==> AUTO
        (g0-p0,e0,g0-p0)-->Tun_2(Stat4*) ==> false
    Discharge ==> Stat5: (Un(p0) * Un(g0-p0) /= 0) & Stat6: (FORALL e in g0 | 0 in {Un(p0)*e,Un(g0-p0)*e})
--
-- Possibility (2) also leads to a contradiction: in fact, if $e1 in p0$ and $v1 in e1$ are
-- such that $v1 in Un(g0-p0)$ then either $Un(p0)*e1$ is null or $Un(g0-p0)*e1$ must be null;
-- but then it is untenable that $v1 in Un(g0-p0)$ holds.
--
    Use_def(Un(p0)) ==> AUTO
    v1-->Stat5(Stat5*) ==> Stat7: (v1 in {u: e in p0, u in e}) & (v1 in Un(p0)*Un(g0-p0))
    (e1,u1)-->Stat7(Stat7,Stat1*) ==> (e1 in g0) & (v1 in e1)
--
-- Both possibilities have led us to contradiction; hence the claim of this theorem holds. 
--
    e1-->Stat6(Stat7*) ==> false
    Discharge ==> QED
--
--
--
Theorem hgraph_d: [The nodes of a singleton graph are the elements of its edge] (nodes({E}) = E) & (nodes(0) = 0). Proof:
Suppose_not(e0) ==> AUTO
    (e0,{e0})-->Tun_4 ==> Un({e0}) = e0
    0-->Tun_0(*) ==> Un(0) = 0
    Use_def(nodes) ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 8 of [CO14].
--
Theorem hgraph_e: [Every vertex is brought in by an edge] (V in nodes(G)) 可mp ((V in edgeOf(V,G)) & (edgeOf(V,G) in G) & (edgeOf(V,G) 可ncin nodes(G))). Proof:
Suppose_not(v0,g0) ==> AUTO
    Use_def(nodes(g0)) ==> AUTO
    Suppose ==> edgeOf(v0,g0) notin {e in g0 | v0 in e}
        Use_def(edgeOf) ==> Stat1: {e in g0 | v0 in e} = 0
        Use_def(Un) ==> Stat2: v0 in {v: e in g0, v in e}
        (e1,v1)-->Stat2(Stat2*) ==> (e1 in g0) & (v0 in e1)
        e1-->Stat1(Stat1*) ==> false
    Discharge ==> Stat3: edgeOf(v0,g0) in {e in g0 | v0 in e}
    ()-->Stat3(*) ==> (edgeOf(v0,g0) in g0) & (v0 in edgeOf(v0,g0)) & (edgeOf(v0,g0) 叩incin Un(g0))
    (g0,edgeOf(v0,g0),g0)-->Tun_2(Stat3*) ==> false
    Discharge ==> QED
--
-- \subsection{Hypergraphs viewed as sets of edges}
--
Def hgraph2: [Hypergraphs seen as sets of edges] HGraph(G) := Finite(nodes(G)) & (FORALL e in G | CardAtLeast2(e))
--
Theorem hgraph0: [An ur-graph] HGraph({{0,{0}}}). Proof:
Suppose_not() ==> AUTO
    Use_def(HGraph) ==> (not Finite(nodes({{0,{0}}}))) or (not (FORALL e in {{0,{0}}} | CardAtLeast2(e)))
    {0,{0}}-->Thgraph_d(*) ==> nodes({{0,{0}}}) = {0,{0}}
    {0}-->Tfin_2(*) ==> Finite({{0}}) & ({0,{0}} = {{0}}+{0})
    ({{0}},0)-->Tfin_1(*) ==> Finite({{0}}+{0})
    EQUAL ==> Stat1: not(FORALL e in {{0,{0}}} | CardAtLeast2(e))
    e1-->Stat1(Stat1*) ==> Stat2: (e1 = {0,{0}}) & (not CardAtLeast2(e1))
    Use_def(CardAtLeast2) ==> not (e1 叩incin {arb(e1)})
    (Stat2)Discharge ==> QED
--
Theorem hgraph1: [Every graph has finitely many edges; and it is null iff its set of nodes is null] HGraph(G) 可mp (Finite(G) & ((G=0) 占q (nodes(G)=0))). Proof:
Suppose_not(g0) ==> AUTO
--
-- A hypothetical counterexample $g0$ cannot be null, else it would be finite and
-- its sum-set would be null; but then, unless finite, $g0$ would equal ${0}$, which
-- conflicts with the fact that every edge must be at least doubleton.
--
    0-->Tfin_2(*) ==> Finite(0)
    g0-->Tun_0(*) ==> (Un(g0) = 0) 占q (g0 可ncin {0})
    Use_def(nodes) ==> Stat1: (not Finite(g0)) or (0 in g0)
    Use_def(HGraph) ==> Stat2: (FORALL e in g0 | CardAtLeast2(e)) & Finite(nodes(g0))
    Use_def(CardAtLeast2) ==> not CardAtLeast2(0)
    0-->Stat2(Stat2*) ==> 0 notin g0
    Use_def(nodes) ==> Finite(Un(g0))
    g0-->Tfin_6(Stat1*) ==> false
    Discharge ==> QED
--
--
Theorem hgraph2: [Every graph edge consists of two or more nodes] (HGraph(G) & (E in G)) 可mp ((E 可ncin nodes(G)) & (E 叩incin {V}) & CardAtLeast2(E)). Proof:
Suppose_not(g0,e0,v0) ==> AUTO
    (g0,e0,g0)-->Tun_2(*) ==> e0 可ncin Un(g0)
    Use_def(nodes(g0)) ==> AUTO
    Use_def(HGraph) ==> Stat1: (FORALL e in g0 | CardAtLeast2(e)) & (e0 in g0) & (not((e0 叩incin {v0}) & CardAtLeast2(e0)))
    e0-->Stat1(Stat1*) ==> CardAtLeast2(e0)
    Use_def(CardAtLeast2) ==> CardAtLeast2(e0) 占q (e0 叩incin {arb(e0)})
    (Stat1)Discharge ==> QED
--
Theorem hgraph3: [Graphs induce subgraphs] (HGraph(G) & (P 可ncin G)) 可mp (HGraph(P) & (nodes(P) 可ncin nodes(G))). Proof:
Suppose_not(g0,p0) ==> AUTO
    Set_monot ==> (FORALL e in g0 | CardAtLeast2(e)) 可mp (FORALL e in p0 | CardAtLeast2(e))
    Use_def(HGraph) ==> Stat1: (nodes(p0) 叩incin nodes(g0)) & (g0 = g0+p0)
    EQUAL(Stat1) ==> nodes(p0) 叩incin nodes(g0+p0)
    (g0,p0)-->Thgraph_b(Stat1*) ==> false
    Discharge ==> QED
--
-- \subsection{Edges incident to a vertex or to a set of vertices}
--
Def hgraph3: [Edges incident to a given node] contains(G,V) := {e in G | V in e}
--
Def hgraph4: [Edges touching a given set] cov(G,P) := {e in G | e * nodes(P) /= 0}
--
-- The following proposition roughly corresponds to Lemma 12 of [CO14].
--
Theorem hgraph4: HGraph(P) 可mp (cov(G,P) = {a: e in P, v in e, a in contains(G,v)}). Proof:
Suppose_not(p0,g0) ==> AUTO
    Use_def(cov) ==> Stat1: {e in g0 | e * nodes(p0) /= 0} /= {a: e in p0, v in e, a in contains(g0,v)}
    e0-->Stat1(Stat1*) ==> Stat2: (e0 in {e in g0 | e * nodes(p0) /= 0}) 叩eq (e0 in {a: e in p0, v in e, a in contains(g0,v)})
    Suppose ==> Stat3: e0 in {a: e in p0, v in e, a in contains(g0,v)}
        (e1,v1,a1)-->Stat3(Stat2*) ==> Stat4: (e0 notin {e in g0 | e * nodes(p0) /= 0}) & (e1 in p0) & (v1 in e1) & (e0 in contains(g0,v1))
        (p0,e1,v1)-->Thgraph2(*) ==> v1 in nodes(p0)
        Use_def(contains(g0,v1)) ==> AUTO
        e0-->Stat4(Stat4*) ==> Stat5: (e0 in {e in g0 | v1 in e}) & ((e0 in g0) 可mp (v1 notin e0))
        ()-->Stat5(Stat5*) ==> false
    Discharge ==> Stat6: (e0 in {e in g0 | e * nodes(p0) /= 0}) & (e0 notin {a: e in p0, v in e, a in contains(g0,v)})
    ()-->Stat6(Stat6*) ==> Stat7: (e0 * nodes(p0) /= 0) & (e0 notin {a: e in p0, v in e, a in contains(g0,v)}) & (e0 in g0)
    (v2,p0)-->Thgraph_e ==> AUTO 
    Use_def(contains(g0,v2)) ==> AUTO
    (v2,edgeOf(v2,p0),v2,e0)-->Stat7(Stat7*) ==> Stat8: (e0 notin {e in g0 | v2 in e}) & (v2 in e0)
    e0-->Stat8(Stat8,Stat7*) ==> false
    Discharge ==> QED
--    
--
--
Theorem hgraph5: HGraph(G) 可mp (cov(G,Q) incs (Q*G)). Proof:
Suppose_not(g0,q0) ==> AUTO
    Use_def(cov) ==> Stat1: ({e in g0 | e * nodes(q0) /= 0} 叩incs (q0*g0)) & (HGraph(g0))
    e0-->Stat1(Stat1*) ==> Stat2: (e0 notin {e in g0 | e * nodes(q0) /= 0}) & (e0 in (q0*g0))
    (g0,e0)-->Thgraph2(Stat1*) ==> (e0 可ncin nodes(g0)) & (e0 /= 0)
    e0-->Stat2(Stat2*) ==> Stat3: (e0 * nodes(q0) = 0) & (e0 in q0)
    ({e0},q0)-->Thgraph_a(Stat3*) ==> e0 * nodes({e0}) = 0 
    e0-->Thgraph_d(Stat2*) ==> false
    Discharge ==> QED    
--
-- The following proposition corresponds to Lemma 13 of [CO14].
--
Theorem hgraph6: (cov(G,P) 可ncin P) 占q (nodes(G-P) * nodes(P) = 0). Proof:
Suppose_not(g0,p0) ==> AUTO
    Use_def(cov(g0,p0)) ==> AUTO
    Use_def(nodes) ==> Stat0: ({e in g0 | e * Un(p0) /= 0} 可ncin p0) 叩eq (Un(g0-p0) * Un(p0) = 0) 
    Suppose ==> Stat1: (Un(g0-p0) * Un(p0) /= 0) & ({e in g0 | e * Un(p0) /= 0} 可ncin p0)
        Use_def(Un(g0-p0)) ==> AUTO
        v0-->Stat1(Stat1*) ==> Stat2: (v0 in {u: v in g0-p0, u in v}) & (v0 in Un(p0))
        (e0,v1)-->Stat2(Stat1*) ==> Stat3: (e0 notin {e in g0 | e * Un(p0) /= 0}) & (e0 in g0) & (v0 in e0)
        e0-->Stat3(Stat2*) ==> false
    Discharge ==> Stat4: ({e in g0 | e * Un(p0) /= 0} 叩incin p0) & (Un(g0-p0) * Un(p0) = 0)
    e1-->Stat4(Stat4*) ==> Stat5: (e1 in {e in g0 | e * Un(p0) /= 0}) & (e1 notin p0)
    ()-->Stat5(Stat5*) ==> (e1 in g0) & (e1 * Un(p0) /= 0)
    (g0-p0,e1,g0-p0)-->Tun_2(Stat4*) ==> false
    Discharge ==> QED
--
--
-- The following proposition corresponds to Lemma 14 of [CO14], which it slightly generalizes.
--
Theorem hgraph7: ((nodes(G) incs nodes(F)) & HGraph(F) & (F incs P) & (P /= 0)) 可mp (cov(G,P) /= 0). Proof:
Suppose_not(g0,f0,p0) ==> Stat0: (p0 /= 0) & (f0 incs p0) & HGraph(f0) & (nodes(g0) incs nodes(f0)) & (cov(g0,p0) = 0)
    (f0,p0)-->Thgraph3(*) ==> HGraph(p0) & (nodes(p0) 可ncin nodes(f0))
    e0-->Stat0(*) ==> e0 in p0
    (p0,e0)-->Thgraph2(*) ==> Stat1: (e0 /= 0) & (e0 可ncin nodes(p0)) & (e0 可ncin nodes(f0))
    v0-->Stat1(*) ==> (v0 in nodes(p0)) & (v0 in nodes(g0))
    (v0,g0)-->Thgraph_e(Stat1*) ==> (v0 in edgeOf(v0,g0)) & (edgeOf(v0,g0) in g0)
    Use_def(cov) ==> Stat2: {e in g0 | e * nodes(p0) /= 0} = 0
    (edgeOf(v0,g0))-->Stat2(Stat1*) ==> false
    Discharge ==> QED
--
-- \subsection{Vertex-removal operation}
--
Def hgraph5: [Filtering out of a graph the edges incident to a fixed vertex] filter(G,V) := {e-{V} : e in G | CardAtLeast2(e-{V})}
--
-- The following proposition roughly corresponds to Lemma 15 of [CO14], which it slightly enriches.
--
Theorem hgraph8: [Filtering transforms graphs into graphs and eliminates at least the operand vertex] (contains(G,V) 可ncin G) & (nodes(filter(G,V)) 可ncin (nodes(G)-{V})) & (HGraph(G) 可mp HGraph(filter(G,V))). Proof:
Suppose_not(g0,v0) ==> AUTO
    Suppose ==> not ( contains(g0,v0) 可ncin g0 )
        Set_monot ==> {e in g0 | v0 in e} 可ncin {e: e in g0}
        Use_def(contains(g0,v0)) ==> AUTO
    Discharge ==> AUTO 
    Suppose ==> nodes(filter(g0,v0)) 叩incin (nodes(g0)-{v0})
        Use_def(nodes) ==> Un(filter(g0,v0)) 叩incin (Un(g0)-{v0})
        Use_def(filter) ==> Stat1: Un({e-{v0} : e in g0 | CardAtLeast2(e-{v0})}) 叩incin (Un(g0)-{v0})
        Use_def(Un({e-{v0}: e in g0 | CardAtLeast2(e-{v0})})) ==> AUTO
        v1-->Stat1(Stat1*) ==> Stat2: (v1 in {u: v in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}, u in v}) & (v1 notin Un(g0)-{v0})
        SIMPLF(Stat2*) ==> Stat3: v1 in {u: e in g0, u in e-{v0} | CardAtLeast2(e-{v0})}
        Use_def(Un(g0)) ==> AUTO
        (e1,u1)-->Stat3(Stat2*) ==> Stat4: (v1 notin {u: e in g0, u in e}) & (e1 in g0) & (v1 in e1) 
        (e1,v1)-->Stat4(Stat4*) ==> false
    Discharge ==> Stat5: (nodes(filter(g0,v0)) 可ncin nodes(g0)) & HGraph(g0) & (not HGraph(filter(g0,v0)))
    g0-->Thgraph1 ==> AUTO
    Use_def(HGraph) ==> Finite(nodes(g0)) & (FORALL e in g0 | CardAtLeast2(e)) & (not(Finite(nodes(filter(g0,v0))) & (FORALL e in filter(g0,v0) | CardAtLeast2(e))))
    Suppose ==> not Finite(filter(g0,v0))
        Use_def(filter) ==> not Finite({e-{v0} : e in g0 | CardAtLeast2(e-{v0})})
        Set_monot ==> {e-{v0}: e in g0 | CardAtLeast2(e-{v0})} 可ncin {e-{v0} : e in g0}
        APPLY() finiteImage(s0->g0,f(X)->(X-{v0})) ==> Finite({e-{v0} : e in g0})
        (Stat5)ELEM ==> false
    Discharge ==> not(FORALL e in filter(g0,v0) | CardAtLeast2(e))
    Use_def(filter) ==> Stat6: not(FORALL a in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})} | CardAtLeast2(a))
    e0-->Stat6(Stat6*) ==> Stat7: (e0 in {e-{v0}: e in g0 | CardAtLeast2(e-{v0})}) & (not CardAtLeast2(e0))
    e-->Stat7 ==> AUTO
    EQUAL(Stat7) ==> false
    Discharge ==> QED
--
--
-- The following proposition corresponds to Lemma 16 of [CO14].
--
Theorem hgraph9: [Covering splitting rule] (HGraph(G) & (nodes(filter(G,V)) = nodes(G)-{V}) & (P 可ncin filter(G,V))) 可mp (cov(G,P)+cov(G,filter(G,V)-P) = G). Proof:
Suppose_not(g0,v0,p0) ==> AUTO
    Use_def(cov) ==> Stat1: {e in g0 | e * nodes(p0) /= 0} + {e in g0 | e * nodes(filter(g0,v0)-p0) /= 0} /= g0
    Set_monot ==> ({e in g0 | e * nodes(p0) /= 0} 可ncin {e in g0 | true})
    Set_monot ==> ({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0} 可ncin {e in g0 | true})
    TELEM ==> {e in g0 | true} = g0
    e0-->Stat1(Stat1*) ==> Stat2: (e0 notin {e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}) & (e0 notin {e in g0 | e * nodes(p0) /= 0}) & (e0 in g0)
    (e0,e0)-->Stat2(Stat2*) ==> e0 * (nodes(filter(g0,v0)-p0)+nodes(p0)) = 0
    EQUAL ==> Stat3: filter(g0,v0)-p0+p0 = filter(g0,v0)
    EQUAL(Stat3) ==> nodes(filter(g0,v0)-p0+p0) = nodes(filter(g0,v0))
    (p0,filter(g0,v0)-p0)-->Thgraph_b(Stat2*) ==> Stat4: e0 * nodes(filter(g0,v0)) = 0
    (g0,e0,v0)-->Thgraph2(*) ==> (e0 可ncin nodes(g0)) & (e0 叩incin {v0}) & (nodes(filter(g0,v0))+{v0} = nodes(g0))
    (g0,v0)-->Thgraph8(Stat4*) ==> false; Discharge ==> QED
--
-- The following proposition corresponds to Lemma 6 of [CO14].
--
Theorem hgraph10: [Basic promoter of the equivalence between connectivity and path connectivity] (HGraph(G) & (P 可ncin filter(G,V)) & (nodes(P) * nodes(filter(G,V)-P) = 0)) 可mp
    (FORALL e in G | 0 in {nodes(P)*e,nodes(filter(G,V)-P)*e}). Proof:
Suppose_not(g0,p0,v0) ==> AUTO
    ELEM ==> Stat0: (not(FORALL e in g0 | 0 in {nodes(p0)*e,nodes(filter(g0,v0)-p0)*e}))
    Use_def(filter(g0,v0)) ==> AUTO
    e0-->Stat0(*) ==> Stat1: (0 /= nodes(filter(g0,v0)-p0)*e0) & (0 /= nodes(p0)*e0) & (e0 in g0) & (p0 可ncin filter(g0,v0)) & (nodes(p0) * nodes(filter(g0,v0)-p0) = 0) & HGraph(g0)
    Use_def(HGraph) ==> Stat2: (FORALL e in g0 | CardAtLeast2(e))
    (p0,filter(g0,v0))-->Thgraph_c(Stat0*) ==> Stat3: (FORALL e in filter(g0,v0) | 0 in {nodes(p0)*e,nodes(filter(g0,v0)-p0)*e})
    (g0,v0)-->Thgraph8 ==> AUTO
    Suppose ==> e0-{v0} = e0
        e0-->Stat2(Stat1*) ==> CardAtLeast2(e0)
        EQUAL ==> CardAtLeast2(e0-{v0})
        Suppose ==> Stat4: e0 notin {e-{v0}: e in g0  | CardAtLeast2(e-{v0})}
        e0-->Stat4(Stat1*) ==> false; Discharge ==> e0 in filter(g0,v0)
        e0-->Stat3(Stat1*) ==> false
    Discharge ==> AUTO
    (v1,v2)-->Stat1(Stat1,Stat1*) ==> Stat5: (v1 in nodes(filter(g0,v0)-p0)*e0) & (v2 in nodes(p0)*e0)
    (p0,filter(g0,v0))-->Thgraph_a(Stat1*) ==> v0 notin nodes(p0)
    (filter(g0,v0)-p0,filter(g0,v0))-->Thgraph_a(Stat3*) ==> (v0 /= v1) & (v0 /= v2)
    Loc_def ==> e1 = e0-{v0}
    Suppose ==> e1 notin filter(g0,v0)
        Use_def(CardAtLeast2) ==> CardAtLeast2(e0-{v0})
        Use_def(filter) ==> Stat6: e1 notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
        e0-->Stat6(Stat1*) ==> false
    Discharge ==> AUTO
    e1-->Stat3(Stat5*) ==> Stat7: nodes(p0) * nodes(filter(g0,v0)-p0) /= 0
    (Stat1,Stat7*)Discharge ==> QED
--
-- The following proposition corresponds to Lemma 17 of [CO14].
--
Theorem hgraph11: [Variant of the basic promoter of the equivalence between connectivity and path connectivity] (HGraph(G) & (P 可ncin filter(G,V)) & (nodes(P) * nodes(filter(G,V)-P) = 0)) 可mp (cov(G,P) * cov(G,filter(G,V)-P) = 0). Proof:
Suppose_not(g0,p0,v0) ==> AUTO
    Use_def(cov) ==> Stat1: {e in g0 | e * nodes(p0) /= 0} * {e in g0 | e * nodes(filter(g0,v0)-p0) /= 0} /= 0
    (g0,p0,v0)-->Thgraph10 ==> AUTO
    e0-->Stat1(*) ==> Stat2: (e0 in {e: e in g0 | e * nodes(p0) /= 0}) & (e0 in {e: e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}) & (FORALL e in g0 | 0 in {nodes(p0)*e,nodes(filter(g0,v0)-p0)*e})
    (e1,e2,e0)-->Stat2(Stat2*) ==> false
    Discharge ==> QED
--
-- \section{Connectivity}
--
Def hgraph6: [Connectivity] Conn(G) := HGraph(G) & ({p 可ncin G | nodes(p) * nodes(G-p) = 0} 可ncin {0,G})
--
Def hgraph7: [Nodes of a graph that get 'accidentally' lost in consequence of filtering] lost(G,V) := nodes(G)-(nodes(filter(G,V))+{V})
--
-- The following proposition corresponds to Lemma 7 of [CO14].
--
Theorem hgraph12: [Covering disjointness rule] (Conn(G) & (P 可ncin filter(G,V)) & (P notin {0,filter(G,V)}) & (V in nodes(G)) & (nodes(P) * nodes(filter(G,V)-P) = 0) & (lost(G,V) = 0)) 可mp
    (nodes(cov(G,P)) * nodes(cov(G,filter(G,V)-P)) = {V}). Proof:
Suppose_not(g0,p0,v0) ==> AUTO
    Use_def(Conn) ==> ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0}) & HGraph(g0)
    (g0,v0)-->Thgraph8 ==> Stat0: AUTO
    Use_def(lost) ==> Stat1: (nodes(filter(g0,v0)) = nodes(g0)-{v0}) & (v0 in nodes(g0))
    (g0,v0,p0)-->Thgraph9(*) ==> cov(g0,p0)+cov(g0,filter(g0,v0)-p0) = g0
    (g0,p0,v0)-->Thgraph11(*) ==> Stat2: cov(g0,filter(g0,v0)-p0) = g0-cov(g0,p0)
    Suppose ==> nodes(cov(g0,filter(g0,v0)-p0)) * nodes(cov(g0,p0)) = 0
        EQUAL(Stat2) ==> nodes(g0-cov(g0,p0)) * nodes(cov(g0,p0)) = 0
        Suppose ==> Stat3: cov(g0,p0) notin {p 可ncin g0 | nodes(p) * nodes(g0-p) = 0}
            (g0,p0)-->Thgraph6 ==> AUTO
            p0-->Stat3(*) ==> false
        Discharge ==> Stat4: (p0 /= 0) & (cov(g0,p0) in {0,g0})
        Use_def(filter(g0,v0)) ==> AUTO
        Use_def(cov(g0,p0)) ==> AUTO
        (g0,filter(g0,v0),p0)-->Thgraph7(*) ==> Stat6: (filter(g0,v0) /= p0) & ({e in g0 | e * nodes(p0) /= 0} = g0)
        ep-->Stat6(*) ==> (ep in filter(g0,v0)) & (ep notin p0)
        (filter(g0,v0),filter(g0,v0)-p0)-->Thgraph3(*) ==> HGraph(filter(g0,v0)-p0) 
        (filter(g0,v0)-p0,ep)-->Thgraph2(*) ==> (ep /= 0) & (ep * nodes(p0) = 0)
        Use_def(filter) ==> Stat7: ep in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
        eq-->Stat7(Stat6*) ==> Stat8: (eq in {e in g0 | e * nodes(p0) /= 0}) & (ep = eq-{v0})
        ()-->Stat8(Stat6*) ==> v0 in nodes(p0)
        (p0,filter(g0,v0))-->Thgraph_a(*) ==> nodes(p0) 可ncin nodes(filter(g0,v0))
    (Stat0*)Discharge ==> AUTO
    Use_def(cov) ==>  Stat9: nodes({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}) * nodes({e in g0 | e * nodes(p0) /= 0}) 叩incin {v0}
    v1-->Stat9(Stat9*) ==> Stat10: (v1 in  nodes({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0})) & (v1 in nodes({e in g0 | e * nodes(p0) /= 0})) & (v1 /= v0)
    Loc_def ==> (e1 = edgeOf(v1,{e in g0 | e * nodes(p0) /= 0})) & (e2 = edgeOf(v1,{e in g0 | e * nodes(filter(g0,v0)-p0) /= 0})) 
    (v1,{e in g0 | e * nodes(p0) /= 0})-->Thgraph_e(Stat10*) ==> Stat11: (e1 in {e in g0 | e * nodes(p0) /= 0}) & (v1 in e1) & (e1 可ncin nodes({e in g0 | e * nodes(p0) /= 0}))
    (v1,{e in g0 | e * nodes(filter(g0,v0)-p0) /= 0})-->Thgraph_e(Stat10*) ==> Stat12: (e2 in {e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}) & (v1 in e2) & (e2 可ncin nodes({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}))
    Suppose ==> not((e1 可ncin nodes(g0)) & (e2 可ncin nodes(g0)))
        Set_monot ==> {e in g0 | e * nodes(p0) /= 0} 可ncin {e in g0 | true}
        Set_monot ==> {e in g0 | e * nodes(filter(g0,v0)-p0) /= 0} 可ncin {e in g0 | true}
        TELEM ==> {e in g0 | true} = g0
        ({e in g0 | e * nodes(p0) /= 0},g0)-->Thgraph_a(Stat12*) ==> nodes({e in g0 | e * nodes(p0) /= 0}) 可ncin nodes(g0)
        ({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0},g0)-->Thgraph_a(Stat12*) ==> nodes({e in g0 | e * nodes(filter(g0,v0)-p0) /= 0}) 可ncin nodes(g0)
    (Stat11*)Discharge ==> Stat13: (e1 可ncin nodes(g0)) & (e2 可ncin nodes(g0)) & (v1 in e1*e2*nodes(g0)) & (filter(g0,v0)-p0+p0=filter(g0,v0))
    ()-->Stat11(Stat11*) ==> (e1 in g0) & (e1 * nodes(p0) /= 0)
    ()-->Stat12(Stat12*) ==> (e2 in g0) & (e2 * nodes(filter(g0,v0)-p0) /= 0)
    (Stat1,Stat1*)ELEM ==> nodes(g0) = nodes(filter(g0,v0)) + {v0}
    (filter(g0,v0)-p0,p0)-->Thgraph_b(Stat12*) ==> nodes(filter(g0,v0)-p0+p0) = nodes(filter(g0,v0)-p0) + nodes(p0)
    EQUAL ==> nodes(g0) = nodes(filter(g0,v0)-p0) + nodes(p0) + {v0}
    (g0,p0,v0)-->Thgraph10(*) ==> Stat14: (FORALL e in g0 | 0 in {nodes(p0)*e,nodes(filter(g0,v0)-p0)*e})
    e1-->Stat14 ==> AUTO
    e2-->Stat14 ==> AUTO
    (Stat13*)ELEM ==> v1 in e1*e2*{v0}
    (Stat9*)Discharge ==> QED
--
-- The following proposition corresponds to Lemma 18 of [CO14].
--
Theorem hgraph13: ((nodes(Q) * nodes(G-Q) = 0) & (P 可ncin G) & Conn(P)) 可mp ((P 可ncin (G-Q)) or (P 可ncin Q)). Proof:
Suppose_not(q0,g0,p0) ==> Stat1: (p0 叩incin (g0-q0)) & (p0 叩incin q0) & (nodes(q0) * nodes(g0-q0) = 0) & (p0 可ncin g0) & Conn(p0)
    Use_def(Conn(p0)) ==> AUTO
    (e0,e1)-->Stat1(Stat1*) ==> Stat2: (p0-q0 notin {p 可ncin p0 | nodes(p) * nodes(p0-p) = 0}) & (p0-(p0-q0) 可ncin q0) & ((p0-q0) 可ncin (g0-q0))
    (p0-q0)-->Stat2(Stat2*) ==> nodes(p0-q0) * nodes(p0-(p0-q0)) /= 0
    (p0-(p0-q0),q0)-->Thgraph_a ==> AUTO
    (p0-q0,g0-q0)-->Thgraph_a(Stat2*) ==> Stat3: nodes(q0) * nodes(g0-q0) /= 0
    (Stat3,Stat1*)Discharge ==> QED
--
-- The following proposition corresponds to Lemma 19 of [CO14].
--
Theorem hgraph14: (Conn(P+Q) & (nodes(P) * nodes(Q) = {V})) 可mp Conn(P). Proof:
Suppose_not(p0,q0,v0) ==> AUTO
    Use_def(Conn) ==> Stat1: ({p 可ncin (p0+q0) | nodes(p) * nodes(p0+q0-p) = 0} 可ncin {0,p0+q0}) & HGraph(p0+q0)
    Use_def(Conn(p0)) ==> AUTO
    (p0+q0,p0)-->Thgraph3(*) ==> Stat2: ({p 可ncin p0 | nodes(p) * nodes(p0-p) = 0} 叩incin {0,p0}) & Conn(p0+q0) & (nodes(p0) * nodes(q0) = {v0})
    p1-->Stat2(Stat2*) ==> Stat3: (p1 in {p 可ncin p0 | nodes(p) * nodes(p0-p) = 0}) & (p1 /= p0) & (p1 /= 0)
    ()-->Stat3(Stat3*) ==> Stat4: (p0-p1+p1 = p0) & (nodes(p1) * nodes (p0-p1) = 0)
    (p0-p1,p1)-->Thgraph_b ==> AUTO
    EQUAL(Stat2) ==> Stat5: {v0} = (nodes(p0-p1) + nodes(p1)) * nodes(q0)
    Suppose ==> Stat6: not(EXISTS p in {p1,p0-p1} | nodes(p) * nodes(q0) = 0)
        p1-->Stat6 ==> AUTO
        (p0-p1)-->Stat6(Stat4*) ==> false
    Discharge ==> Stat7: (EXISTS p in {p1,p0-p1} | nodes(p) * nodes(q0) = 0)
    p2-->Stat7(Stat7*) ==>  Stat8: (p2 in {p1,p0-p1}) & (nodes(p2) * nodes(q0) = 0)
    Suppose ==> nodes(p2) * nodes(p0-p2) /= 0
        Suppose ==> p2 = p1
        EQUAL(Stat4) ==> false; Discharge ==> (p2 = p0-p1)  & (p1 = p0-(p0-p1))
        EQUAL(Stat5) ==> Stat9: nodes(p0-p1) * nodes(p1) /= 0 
    (Stat4,Stat9*)Discharge ==> AUTO
    Suppose ==> Stat10: p2 * q0 /= 0
        e0-->Stat10(Stat4,Stat8,Stat10*) ==> (e0 in p0) & (e0 in q0)
        (p0+q0,p0)-->Thgraph3(Stat1,Stat1*) ==> HGraph(p0)
        (p0,e0,v0)-->Thgraph2(Stat10*) ==> (e0 可ncin nodes(p0)) & (e0 叩incin {v0})
        (p0+q0,q0)-->Thgraph3(Stat1,Stat1*) ==> HGraph(q0)
        (q0,e0,v0)-->Thgraph2(Stat10*) ==> nodes(p0) * nodes(q0) /= {v0}
        EQUAL ==> false
    Discharge ==> AUTO
    (p0-p2,q0)-->Thgraph_b ==> AUTO
    (Stat8*)ELEM ==> Stat11: (0 = nodes(p2) * nodes(p0-p2+q0)) & (p0-p2+q0 = p0+q0-p2)
    EQUAL(Stat11) ==> 0 = nodes(p2) * nodes(p0+q0-p2)
    (Stat8,Stat3,Stat4,Stat1*)ELEM ==> Stat12: (p2 notin {p 可ncin (p0+q0) | nodes(p) * nodes(p0+q0-p) = 0}) & (p2 可ncin (p0+q0))
    p2-->Stat12(Stat11*) ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 20 of [CO14].
--
Theorem hgraph15: (HGraph(P+Q) & (nodes(P)*nodes(Q) = {V}) & (W in nodes(Q)-{V})) 可mp (P 可ncin filter(P+Q,W)). Proof:
Suppose_not(p0,q0,v0,w0) ==> Stat2: (p0 叩incin filter(p0+q0,w0)) & (w0 in nodes(q0)-{v0}) & (w0 notin nodes(p0)) & HGraph(p0+q0) & (nodes(p0)*nodes(q0) = {v0})
    Use_def(filter) ==> p0 叩incin {e-{w0}: e in p0+q0 | CardAtLeast2(e-{w0})}
    Set_monot ==> {e-{w0}: e in p0 | CardAtLeast2(e-{w0})} 可ncin {e-{w0}: e in p0+q0 | CardAtLeast2(e-{w0})}
    (Stat2*)ELEM ==> Stat3: p0 叩incin {e-{w0}: e in p0 | CardAtLeast2(e-{w0})}
    e1-->Stat3(Stat3*) ==> Stat4: (e1 notin {e-{w0}: e in p0 | CardAtLeast2(e-{w0})}) & (e1 in p0)
    e1-->Stat4(Stat4*) ==> (w0 in e1) or (not CardAtLeast2(e1-{w0}))
    (p0+q0,p0)-->Thgraph3(Stat2*) ==> HGraph(p0)
    (p0,e1)-->Thgraph2(Stat2*) ==> (e1-{w0} in p0) & (not CardAtLeast2(e1-{w0})) 
    Use_def(HGraph) ==> Stat5: (FORALL e in p0 | CardAtLeast2(e))
    (e1-{w0})-->Stat5(Stat4*) ==> false
    Discharge ==> QED
--
Theorem hgraph16: [Trivial connected graphs] ((HGraph({E}) & (P 可ncin {E})) 可mp Conn(P)) & Conn(0). Proof:
Suppose_not(e0,p0) ==> AUTO
    Suppose ==> not Conn(0)
        ({{0,{0}}},0)-->Thgraph3 ==> AUTO
        ()-->Thgraph0 ==> AUTO
        Use_def(Conn) ==> Stat1: {p 可ncin 0 | nodes(p) * nodes(0-p) = 0} 叩incin {0}
        q0-->Stat1(Stat1*) ==> Stat2: (q0 in {p 可ncin 0 | nodes(p) * nodes(0-p) = 0}) & (q0 /= 0)
        ()-->Stat2(Stat2*) ==> false
    Discharge ==> AUTO       
    ({e0},p0)-->Thgraph3 ==> HGraph(p0)
    Use_def(Conn) ==> Stat6: {p 可ncin p0 | nodes(p) * nodes(p0-p) = 0} 叩incin {0,p0}
    p1-->Stat6(Stat6*) ==> Stat7: (p1 in {p 可ncin p0 | nodes(p) * nodes(p0-p) = 0}) & (p1 notin {0,p0})
    ()-->Stat7(*) ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 21 of [CO14].
--
Theorem hgraph17: (HGraph(G) & (FORALL v in nodes(G) | filter(G,v) * G = 0)) 可mp (FORALL v in nodes(G) | Conn(filter(G,v))). Proof:
Suppose_not(g0) ==> Stat1: (FORALL v in nodes(g0) | filter(g0,v) * g0 = 0) & Stat2: (not(FORALL v in nodes(g0) | Conn(filter(g0,v)))) & HGraph(g0)
    Suppose ==> Stat4: not(FORALL v in nodes(g0) | contains(g0,v) = g0)
        (g0,v0)-->Thgraph8(Stat4*) ==> contains(g0,v0) 可ncin g0
        Use_def(contains(g0,v0)) ==> AUTO
        v0-->Stat4(Stat4*) ==> Stat5: (g0 叩incin {e in g0 | v0 in e}) & (v0 in nodes(g0))
        v0-->Stat1(Stat5*) ==> filter(g0,v0) * g0 = 0
        Use_def(filter(g0,v0)) ==> AUTO
        e0-->Stat5(Stat5*) ==> Stat6: (e0 notin {e in g0 | v0 in e}) & (e0 notin {e-{v0}: e in g0 | CardAtLeast2(e-{v0})}) & (e0 in g0)
        (e0,e0)-->Stat6(Stat6*) ==> (e0=e0-{v0}) & (not CardAtLeast2(e0-{v0}))
        EQUAL(Stat6) ==> not CardAtLeast2(e0)
        Use_def(HGraph) ==> Stat7: (FORALL e in g0 | CardAtLeast2(e))
        e0-->Stat7(Stat6*) ==> false
    Discharge ==> AUTO
    Loc_def ==> e1 = edgeOf(w,g0)
    w-->Stat2(Stat1*) ==> Stat8: (w in nodes(g0)) & (not Conn(filter(g0,w)))   
    (w,g0)-->Thgraph_e(Stat1*) ==> Stat9: e1 in g0
    Suppose ==> Stat10: g0 /= {e1}
        e2-->Stat10(Stat1*) ==> Stat11: (e2 /= e1) & (FORALL v in nodes(g0) | contains(g0,v) = g0) & (e2 in g0) & HGraph(g0)
        (v1,v1)-->Stat11(Stat11*) ==> ((v1 in e2) 占q (v1 notin e1)) & ((v1 in nodes(g0)) 可mp (contains(g0,v1) = g0))
        (g0,e1,v1)-->Thgraph2 ==> AUTO
        Use_def(contains(g0,v1)) ==> AUTO
        (g0,e2,v1)-->Thgraph2(Stat9*) ==> Stat12: (e1 in {e: e in g0 | v1 in e}) & (e2 in {e: e in g0 | v1 in e})
        (e3,e4)-->Stat12(Stat11*) ==> false
    Discharge ==> AUTO
    Use_def(filter) ==> Stat13: (filter(g0,w) = {e-{w} : e in g0 | CardAtLeast2(e-{w})}) & (g0 = {e1})
    EQUAL(Stat1,Stat13) ==> (filter(g0,w) = {e-{w} : e in {e1} | CardAtLeast2(e-{w})}) & HGraph({e1})
    Suppose ==> not CardAtLeast2(e1-{w})
        Suppose ==> Stat14: {e-{w} : e in {e1} | CardAtLeast2(e-{w})} /= 0
            e5-->Stat14(Stat14*) ==> (e5 = e1) & CardAtLeast2(e5-{w})
            EQUAL(Stat13) ==> false
        Discharge ==> AUTO
        (e1,filter(g0,w))-->Thgraph16(Stat8*) ==> false
    Discharge ==> AUTO
    Suppose ==> Stat15: {e-{w} : e in {e1} | CardAtLeast2(e-{w})} /= {e1-{w}}
        e6-->Stat15(Stat15*) ==> (e6 in {e-{w} : e in {e1} | CardAtLeast2(e-{w})}) 叩eq (e6 = e1-{w})
        Suppose ==> Stat16: e6 notin {e-{w} : e in {e1} | CardAtLeast2(e-{w})}
        e1-->Stat16(Stat13*) ==> false; Discharge ==> AUTO
        (Stat15*)ELEM ==> Stat17: (e6 in {e-{w} : e in {e1} | CardAtLeast2(e-{w})}) & (e6 /= e1-{w})
        e7-->Stat17(Stat17*) ==> false
    Discharge ==> {e-{w} : e in {e1} | CardAtLeast2(e-{w})} = {e1-{w}}
    (g0,w)-->Thgraph8(Stat1,Stat1*) ==> HGraph(filter(g0,w))
    EQUAL(Stat13) ==> HGraph({e1-{w}})
    (e1-{w},filter(g0,w))-->Thgraph16(Stat8*) ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 2 of [CO14].
--
Theorem hgraph18: [A node $W$ other than $V$ gets lost when $V$ is removed from a graph iff ${V,W}$ is the only edge to which $V$ belongs] HGraph(G) 可mp ((W in lost(G,V)) 占q (contains(G,W) = {{V,W}})). Proof:
Suppose_not(g0,v1,v0) ==> AUTO
    Use_def(lost) ==> Stat0: HGraph(g0) & (lost(g0,v0) = nodes(g0)-(nodes(filter(g0,v0))+{v0}))
    Use_def(contains) ==> contains(g0,v1) = {e in g0 | v1 in e}
    (g0,v0)-->Thgraph8(Stat0*) ==> Stat1: (nodes(filter(g0,v0)) 可ncin (nodes(g0)-{v0})) & HGraph(filter(g0,v0))
    Use_def(filter) ==> filter(g0,v0) = {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
    Suppose ==> Stat2: (contains(g0,v1) /= {{v0,v1}}) & (v1 in lost(g0,v0))
        Loc_def ==> e0 = edgeOf(v1,g0)
        (v1,g0)-->Thgraph_e(Stat0*) ==> Stat3: (v1 in e0) & (e0 in g0) & (v1 notin nodes(filter(g0,v0))) & (v1 /= v0)
        Suppose ==> Stat4: e0 notin {e in g0 | v1 in e}
        e0-->Stat4(Stat3*) ==> false; Discharge ==> AUTO
        Suppose ==> v0 notin e0
            Suppose ==> Stat5: e0 notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
                e0-->Stat5(Stat3*) ==> (not CardAtLeast2(e0-{v0})) & (e0-{v0} = e0)
                (g0,e0,0)-->Thgraph2(Stat0*) ==> CardAtLeast2(e0)
                EQUAL(Stat5) ==> false
            Discharge ==> Stat6: e0 in filter(g0,v0)
            (filter(g0,v0),e0,0)-->Thgraph2(Stat1*) ==> false 
        Discharge ==> AUTO
        Suppose ==> e0 = {v0,v1}
             e1-->Stat2(Stat0*) ==> Stat7: (e1 in {e in g0 | v1 in e}) & (e1 /= {v0,v1})
             ()-->Stat7(Stat7*) ==> (e1 in g0) & (v1 in e1)
             (filter(g0,v0),e1,v1)-->Thgraph2(Stat1*) ==> Stat8: e1 notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
             (g0,e1,v1)-->Thgraph2(Stat0*) ==> CardAtLeast2(e1) & (e1 叩incin {v1})
             Suppose ==> e1-{v0} = e1
                 EQUAL ==> CardAtLeast2(e1-{v0})
                 e1-->Stat8(Stat7*) ==> false
             Discharge ==> AUTO
             (Stat3*)ELEM ==> e1-{v0} 叩incin nodes(filter(g0,v0))
             (filter(g0,v0),e1-{v0},0)-->Thgraph2(Stat1*) ==> Stat9: e1-{v0} notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
             Use_def(CardAtLeast2) ==> CardAtLeast2(e1-{v0}) 占q ((e1-{v0}) 叩incin {arb(e1-{v0})})
             e1-->Stat9(Stat3*) ==> false
        Discharge ==> AUTO
        (filter(g0,v0),e0-{v0},0)-->Thgraph2(Stat1*) ==> Stat10: e0-{v0} notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
        Use_def(CardAtLeast2) ==> CardAtLeast2(e0-{v0}) 占q ((e0-{v0}) 叩incin {arb(e0-{v0})})
        e0-->Stat10(Stat3*) ==> false
    Discharge ==> AUTO
    Loc_def ==> Stat11: (e2 = {v0,v1}) & (e3 = edgeOf(v1,filter(g0,v0)))
    ELEM ==> Stat12: (e2 in {e in g0 | v1 in e}) & (v1 notin (nodes(g0)-(nodes(filter(g0,v0))+{v0}))) & ({e in g0 | v1 in e} 可ncin {e2})
    (g0,e2,v1)-->Thgraph2 ==> AUTO
    ()-->Stat12(Stat0*) ==> Stat13: (e2 in g0) & (v0 /= v1) & (v1 in nodes(filter(g0,v0)))
    (v1,filter(g0,v0))-->Thgraph_e(Stat1*) ==> Stat14: (e3 in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}) & (v1 in e3)
    e4-->Stat14(Stat14*) ==> (e3 = e4-{v0}) & (e4 in g0) & CardAtLeast2(e4-{v0})
    Suppose ==> e4 /= e2
        (Stat12*)ELEM ==> Stat15: e4 notin {e in g0 | v1 in e}
        e3-->Stat15(Stat13*) ==> false
    Discharge ==> e4 = e2 
    Use_def(CardAtLeast2) ==> CardAtLeast2(e4-{v0}) 占q ((e4-{v0}) 叩incin {arb(e4-{v0})})
    EQUAL(Stat14) ==> Stat16: (e2-{v0}) 叩incin {arb(e2-{v0})}
    (Stat11,Stat16*)Discharge ==> QED
--
-- The following proposition corresponds to Lemma 3 of [CO14].
--
Theorem hgraph19: [If a node belongs to exactly one edge, $E$, and that $E$ is a doubleton, removal of $E$ does not disrupt connectivity] (Conn(G) & (contains(G,V) = {{V,W}})) 可mp Conn(G-contains(G,V)). Proof:
Suppose_not(g0,v0,v1) ==> AUTO
    (g0,g0-contains(g0,v0))-->Thgraph3 ==> AUTO
    Use_def(Conn) ==> Stat1: ({p 可ncin (g0-contains(g0,v0)) | nodes(p) * nodes(g0-contains(g0,v0)-p) = 0} 叩incin {0,g0-contains(g0,v0)}) &
         HGraph(g0) & ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0}) & (contains(g0,v0) = {{v0,v1}})
    p0-->Stat1(*) ==> Stat2: (p0 in {p 可ncin (g0-contains(g0,v0)) | nodes(p) * nodes(g0-contains(g0,v0)-p) = 0}) & (p0 /= 0) & (p0 /= g0-contains(g0,v0))
    ()-->Stat2(Stat1*) ==> Stat3: (p0 notin {p 可ncin g0 | nodes(p) * nodes(g0-p) = 0}) & (g0-p0=(g0-contains(g0,v0)-p0)+((g0-p0)*contains(g0,v0))) & (p0 可ncin (g0-contains(g0,v0))) & (nodes(p0) * nodes(g0-contains(g0,v0)-p0) = 0)
    p0-->Stat3(Stat2*) ==> (nodes(p0) * nodes(g0-p0)) /= 0
    (g0-contains(g0,v0)-p0,(g0-p0)*contains(g0,v0))-->Thgraph_b ==> AUTO
    EQUAL(Stat3) ==> nodes(p0) * (nodes(g0-contains(g0,v0)-p0) + nodes((g0-p0)*contains(g0,v0))) /= 0
    (Stat2*)ELEM ==> Stat4: nodes(p0) * nodes((g0-p0)*contains(g0,v0)) /= 0    
    Suppose ==> (g0-p0)*contains(g0,v0) = 0
        EQUAL(Stat3) ==> Stat5: nodes(0) /= 0
        0-->Thgraph_d(Stat5*) ==> false
    Discharge ==> Stat6: ({v0,v1} in g0) & ({v0,v1} notin p0)
    Suppose ==> v0 in nodes(p0)
        Set_monot ==> {e in p0 | v0 in e} 可ncin {e in g0 | v0 in e}
        Use_def(contains) ==> {e in p0 | v0 in e} 可ncin contains(g0,v0)
        Suppose ==> Stat7: {v0,v1} in {e in p0 | v0 in e}
        ()-->Stat7(Stat6*) ==> false; Discharge ==> AUTO
        (Stat1*)ELEM ==> Stat8: {e in p0 | v0 in e} = 0
        (v0,p0)-->Thgraph_e(Stat6*) ==> (v0 in edgeOf(v0,p0)) & (edgeOf(v0,p0) in p0)
        (edgeOf(v0,p0))-->Stat8(Stat8*) ==> false
    Discharge ==> AUTO
    Suppose ==> v1 notin nodes(p0)
        ({v0,v1})-->Thgraph_d ==> AUTO
        EQUAL(Stat1) ==> nodes(contains(g0,v0)) = {v0,v1}
        ((g0-p0)*contains(g0,v0),contains(g0,v0))-->Thgraph_a(Stat4*) ==> false
    Discharge ==> Stat9: v1 in nodes(p0)
    Suppose ==> nodes(p0 + contains(g0,v0)) /= nodes(p0) + {v0}
        (p0,contains(g0,v0))-->Thgraph_b ==> AUTO
        ({v0,v1})-->Thgraph_d(Stat9*) ==> nodes(p0) + nodes({{v0,v1}}) = nodes(p0) + {v0}
        EQUAL(Stat1) ==> false
    Discharge ==> (nodes(p0 + contains(g0,v0)) = nodes(p0) + {v0}) & (nodes(g0-contains(g0,v0)-p0) * (nodes(p0) + {v0}) = nodes(g0-contains(g0,v0)-p0) * {v0}) & (g0-(p0+contains(g0,v0)) = g0-contains(g0,v0)-p0)
    EQUAL(Stat6) ==> Stat11: nodes(g0-(p0+contains(g0,v0))) * nodes(p0 + contains(g0,v0)) = nodes(g0-contains(g0,v0)-p0) * {v0}
    Use_def(contains(g0,v0)) ==> AUTO
    Suppose ==> v0 in nodes(g0-contains(g0,v0)-p0)
        (g0-contains(g0,v0)-p0,g0-contains(g0,v0))-->Thgraph_a(Stat11*) ==> v0 in nodes(g0-contains(g0,v0))
        (v0,g0-contains(g0,v0))-->Thgraph_e(Stat11*) ==> Stat12: (edgeOf(v0,g0-contains(g0,v0)) notin {e in g0 | v0 in e}) & (edgeOf(v0,g0-contains(g0,v0)) in g0) & (v0 in edgeOf(v0,g0-contains(g0,v0)))
        (edgeOf(v0,g0-contains(g0,v0)))-->Stat12(Stat12*) ==> false
    Discharge ==> AUTO
    (Stat11*)ELEM ==> nodes(p0 + contains(g0,v0)) * nodes(g0-(p0+contains(g0,v0))) = 0
    Suppose ==> Stat13: (p0 + contains(g0,v0)) notin {p 可ncin g0 | nodes(p) * nodes(g0-p) = 0}
        (p0 + contains(g0,v0))-->Stat13(Stat11*) ==> (p0 + contains(g0,v0)) 叩incin g0
        (g0,v0)-->Thgraph8(Stat2*) ==> false
    Discharge ==> Stat14: AUTO
    (Stat1,Stat2,Stat6,Stat14*)ELEM ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Lemma 4 of [CO14].
--
Theorem hgraph20: [Removal of a node that belongs to exactly one edge does not disrupt connectivity] (Conn(G) & (contains(G,V) = {E})) 可mp Conn(filter(G,V)). Proof:
Suppose_not(g0,v0,e0) ==> AUTO
    Use_def(contains(g0,v0)) ==> AUTO
    Use_def(filter) ==> Stat1: (e0 in {e in g0 | v0 in e}) & ({e in g0 | v0 in e} 可ncin {e0}) & Conn(g0) & (not Conn(filter(g0,v0))) & (filter(g0,v0)={e-{v0} : e in g0 | CardAtLeast2(e-{v0})})
    ()-->Stat1(Stat1*) ==> Stat2: (e0 in g0) & (v0 in e0)
    Use_def(Conn) ==> HGraph(g0) & ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0})
    (g0,e0,v0)-->Thgraph2(Stat1*) ==> Stat3: e0 叩incin {v0}
    Suppose ==> not CardAtLeast2(e0-{v0})
        Use_def(CardAtLeast2) ==> Stat4: (e0-{v0}) 可ncin {arb(e0-{v0})}
        v1-->Stat3(Stat2*) ==> e0 = {v0,v1}
        Suppose ==> Stat5: {e-{v0} : e in g0 | CardAtLeast2(e-{v0})} /= g0-{e0}
            ep-->Stat5 ==> AUTO
            Suppose ==> Stat6: ep in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
                e1-->Stat6(Stat5*) ==> (ep = e1-{v0}) & (e1 in g0) & CardAtLeast2(e1-{v0}) & (ep notin g0-{e0})
                Suppose ==> e1 = e0
                EQUAL(Stat3) ==> false; Discharge ==> AUTO
                (Stat1*)ELEM ==> Stat7: e1 notin {e in g0 | v0 in e}
                e1-->Stat7(Stat6*) ==> e1 = e0
                EQUAL(Stat3) ==> false
            Discharge ==> AUTO
            (Stat1*)ELEM ==> Stat8: (ep notin {e in g0 | v0 in e}) & (ep notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}) & (ep in g0-{e0})
            (ep,ep)-->Stat8(Stat8*) ==> (ep-{v0} = ep) & (not CardAtLeast2(ep-{v0}))
            (g0,ep,0)-->Thgraph2(Stat2) ==> CardAtLeast2(ep)
            EQUAL(Stat8) ==> false
        Discharge ==> filter(g0,v0) = g0-{e0}
        (g0,v0,v1)-->Thgraph19(Stat1*) ==> (contains(g0,v0)={{v0,v1}}) 可mp Conn(g0-contains(g0,v0))    
        EQUAL ==> false
    Discharge ==> AUTO
    Suppose ==> Stat9: {e-{v0} : e in g0 | CardAtLeast2(e-{v0})} /= g0-{e0}+{e0-{v0}}
        eq-->Stat9 ==> AUTO
        Suppose ==> Stat10: eq in {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}
            e2-->Stat10(Stat9*) ==> (eq = e2-{v0}) & (e2 in g0) & CardAtLeast2(e2-{v0}) & (eq notin g0-{e0}+{e0-{v0}})
            Suppose ==> e2 = e0
            EQUAL(Stat3) ==> false; Discharge ==> AUTO
            (Stat1*)ELEM ==> Stat11: e2 notin {e in g0 | v0 in e}
            e2-->Stat11(Stat10*) ==> e2 = e0
            EQUAL(Stat3) ==> false
        Discharge ==> Stat13: (eq notin {e-{v0} : e in g0 | CardAtLeast2(e-{v0})}) & (eq notin {e in g0 | v0 in e}) & (eq in g0-{e0}+{e0-{v0}})
        Suppose ==> eq = e0-{v0}
        e0-->Stat13(Stat2*) ==> false; Discharge ==> AUTO
        (eq,eq)-->Stat13(Stat13*) ==> (eq-{v0} = eq) & (not CardAtLeast2(eq-{v0}))
        (g0,eq,0)-->Thgraph2(Stat2) ==> CardAtLeast2(eq)
        EQUAL(Stat13) ==> false
    Discharge ==> Stat14: filter(g0,v0) = g0-{e0}+{e0-{v0}}
    (g0,v0)-->Thgraph8 ==> AUTO
    Use_def(Conn) ==> Stat15: {p 可ncin filter(g0,v0) | nodes(p) * nodes(filter(g0,v0)-p) = 0} 叩incin {0,filter(g0,v0)}
    p0-->Stat15(Stat15*) ==> Stat16: (p0 in {p 可ncin filter(g0,v0) | nodes(p) * nodes(filter(g0,v0)-p) = 0}) & (p0 /= 0) & (p0 /= filter(g0,v0))
    ()-->Stat16(Stat16*) ==> (p0 可ncin filter(g0,v0)) & (nodes(p0) * nodes(filter(g0,v0)-p0) = 0)
    Loc_def ==> p1 = if (e0-{v0} in p0) then filter(g0,v0)-p0 else p0 end if
    Suppose ==> nodes(p1) * nodes(filter(g0,v0)-p1) /= 0
        Suppose ==> p1 = p0
        EQUAL(Stat16) ==> false; Discharge ==> AUTO
        (Stat16*)ELEM ==> (p1 = filter(g0,v0)-p0) & (filter(g0,v0)-p1 = p0)
        EQUAL(Stat16) ==> nodes(filter(g0,v0)-p0) * nodes(p0) /= 0
    (Stat16*)Discharge ==> AUTO
    (Stat16*)ELEM ==> Stat17: (p1 /= 0) & (p1 /= filter(g0,v0)) & (p1 可ncin filter(g0,v0)) & (nodes(p1) * nodes(filter(g0,v0)-p1) = 0)
    Suppose ==> v0 in nodes(g0-{e0})
         Loc_def ==> e4 = edgeOf(v0,g0-{e0})
         (v0,g0-{e0})-->Thgraph_e(Stat17*) ==> Stat18: (v0 in e4) & (e4 in g0-{e0})
         (Stat1,Stat18*)ELEM ==>Stat19: e4 notin {e in g0 | v0 in e}
         e4-->Stat19(Stat18*) ==> false
    Discharge ==> AUTO
    Suppose ==> nodes(filter(g0,v0)-p1) /= (nodes(g0-p1)-{v0})
        (Stat2,Stat2*)ELEM ==> (e0 in g0) & (v0 in e0)
        (Stat14*)ELEM ==> ((g0-{e0}+{e0-{v0}}-p1 = (g0-{e0}-p1)+{e0-{v0}})) & (g0-{e0}-p1+{e0} = g0-p1)
        (g0-{e0}-p1,{e0-{v0}})-->Thgraph_b ==> AUTO
        (e0-{v0})-->Thgraph_d ==> AUTO
        e0-->Thgraph_d ==> AUTO
        (g0-{e0}-p1,g0-{e0})-->Thgraph_a(Stat17*) ==> nodes(g0-{e0}-p1)+(nodes({e0})-{v0}) = (nodes(g0-{e0}-p1)+nodes({e0}))-{v0}
        (g0-{e0}-p1,{e0})-->Thgraph_b ==> AUTO
        EQUAL(Stat14) ==> false
    Discharge ==> AUTO
    (p1,filter(g0,v0))-->Thgraph_a(Stat3*) ==> nodes(p1) * nodes(g0-p1) = 0
    (Stat2*)ELEM ==> Stat20: (p1 notin {p 可ncin g0 | nodes(p) * nodes(g0-p) = 0}) & (p1 可ncin g0) & (p1 /= g0)
    p1-->Stat20(Stat17*) ==> false
    Discharge ==> QED
--
-- The following proposition reflects an initial remark, or 'prelude', inside the proof of Theorem 2 of [CO14].
--
Theorem hgraph21: [Prelude to Theorem hgraph22] (Conn(G) & (W in nodes(G)) & (not (EXISTS v in nodes(G) | Conn(filter(G,v))))) 可mp ((lost(G,W) = 0) & (nodes(G) = nodes(filter(G,W))+{W})). Proof:
Suppose_not(g0,w0) ==> AUTO
    Use_def(Conn) ==> Stat1: (not(EXISTS v in nodes(g0) | Conn(filter(g0,v)))) & HGraph(g0) & ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0}) & (w0 in nodes(g0)) & (not((lost(g0,w0) = 0) & (nodes(g0) = nodes(filter(g0,w0))+{w0})))
        Suppose ==> Stat2: (EXISTS v | lost(g0,v) /= 0)
            v0-->Stat2(Stat2*) ==> Stat3: lost(g0,v0) /= 0
            v1-->Stat3(Stat3*) ==> v1 in lost(g0,v0)
            (g0,v1,v0)-->Thgraph18(Stat1*) ==> contains(g0,v1) = {{v0,v1}}
            (g0,v1,{v0,v1})-->Thgraph20(*) ==> Conn(filter(g0,v1))
            Use_def(lost(g0,v0)) ==> AUTO
            v1--> Stat1(Stat3*) ==> false
        Discharge ==> Stat4: not(EXISTS v | lost(g0,v) /= 0)
        w0-->Stat4(Stat4*) ==> lost(g0,w0) = 0
        Suppose ==> Stat5: not(FORALL v in nodes(g0) | nodes(g0) = nodes(filter(g0,v))+{v})
            v3-->Stat5(Stat5*) ==> (v3 in nodes(g0)) & (nodes(g0) /= nodes(filter(g0,v3))+{v3})
            Use_def(lost(g0,v3)) ==> AUTO
            (g0,v3)-->Thgraph8 ==> AUTO
            v3-->Stat4(Stat4*) ==> false
        Discharge ==> AUTO
        (Stat4*)ELEM ==> Stat6: (FORALL v in nodes(g0) | nodes(g0) = nodes(filter(g0,v))+{v})
        w0-->Stat6(Stat1*) ==> false
    Discharge ==> QED
--
-- The following proposition corresponds to Theorem 2 of [CO14].
--
Theorem hgraph22: [Every non-null connected graph has a vertex whose removal does not disrupt connectivity] (Conn(G) & (G /= 0)) 可mp (EXISTS v in nodes(G) | Conn(filter(G,v))). Proof:
Suppose_not(g0) ==> AUTO
--
-- Arguing by contradiction, suppose that a connected non-null graph $g0$ exists
-- such that $Conn(filter(g0,v))$ does not node for any of its nodes $v$.
-- Recall that $g0$ is finite and has a non-null set of nodes.  
--
    Use_def(Conn) ==> Stat1: (not(EXISTS v in nodes(g0) | Conn(filter(g0,v)))) & HGraph(g0) & ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0}) & (g0 /= 0)
    g0-->Thgraph1(Stat1*) ==> Stat2: (nodes(g0) /= 0) & Finite(g0)
--
-- Consider the set
--		${p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}$
-- of all connected subgraphs of $g0$ which are included in $filter(g0,v)$ for some node $v$ of $g0$.
-- This set is non-null, because $0$ belongs to it. 
--
    Suppose ==> Stat3: {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))} = 0
--
-- In fact, $0$ is a connected graph. Moreover, it is included in $g0$
-- and satisfies whichever inclusion of the form $0 可ncin X$.
--
        0-->Thgraph16(Stat3*) ==> Conn(0)
        0-->Stat3(Stat3*) ==> Stat4: not(EXISTS v in nodes(g0) | 0 可ncin filter(g0,v))
        v0-->Stat2(Stat4*) ==> v0 in nodes(g0)
        v0-->Stat4(Stat4*) ==> false
    Discharge ==> AUTO
--
-- The finiteness of $g0$ yields the finiteness of $pow(g0)$ and, consequently, the finiteness
-- of any subset of $pow(g0)$: in particular, the set of subgraphs of $g0$ introduced above
-- is finite; therefore it has an inclusion-maximal element $m0$. 
--
    g0-->Tfin_5(Stat2*) ==> Finite(pow(g0))
    Set_monot ==> {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))} 可ncin {x: x 可ncin g0}
    Use_def(pow) ==> Finite({p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))})
    {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}-->Tfin_4(Stat2*) ==> Stat5: (EXISTS m in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))} | {x in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}-{m} | m 可ncin x} = 0)
--
-- That is, the relationship
--		$m0 in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}$
-- holds, and no alike relation holds for a set $m$ strictly included in $m0$. Plainly,
-- $m0$ is a connected subgraph of $g0$ and there is a node $w0$ such that $m0$ is also a subgraph
-- of $filter(g0,v)$. 
--
    m0-->Stat5(Stat5*) ==> Stat7: (m0 in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}) & Stat8: ({x in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}-{m0} | m0 可ncin x} = 0)
    ()-->Stat7(Stat7*) ==> Stat9: (EXISTS v in nodes(g0) | m0 可ncin filter(g0,v)) & (m0 可ncin g0) & Conn(m0)
    w0-->Stat9(Stat9*) ==> (w0 in nodes(g0)) & (m0 可ncin (g0 * filter(g0,w0)))
--
-- Notice that $m0=0$ cannot hold; for, otherwise, it would turn out that $filter(g0,v) * g0 = 0$
-- for every node $v$. But then, by Theorem hgraph17, each graph of the form $filter(g0,v)$, with
-- $v$ a node of $g0$, would be connected; however, we are working under the assumption that
-- no such graph is connected and therefore must discard the possibility that $m0=0$.
--
    Suppose ==> Stat10: m0 = 0
        Suppose ==> Stat11: not(FORALL v in nodes(g0) | filter(g0,v) * g0 = 0)
            w2-->Stat11(Stat11*) ==> Stat12: (filter(g0,w2) * g0 /= 0) & (w2 in nodes(g0)) 
            e1-->Stat12(Stat12*) ==> Stat13: (e1 in filter(g0,w2)) & (e1 in g0)
            (g0,{e1})-->Thgraph3(Stat1,Stat13*) ==> HGraph({e1})
            (e1,{e1})-->Thgraph16(Stat13*) ==> Conn({e1})
            e1-->Stat8(Stat7,Stat7*) ==> Stat14: {e1} notin {x in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}-{m0} | m0 可ncin x}
            {e1}-->Stat14(Stat10*) ==> Stat15: {e1} notin {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}
            {e1}-->Stat15(Stat13*) ==> Stat16: not(EXISTS v in nodes(g0) | {e1} 可ncin filter(g0,v))
            w2-->Stat16(Stat12*) ==> false
        Discharge ==> AUTO
        g0-->Thgraph17(Stat1*) ==> Stat17: (FORALL v in nodes(g0) | Conn(filter(g0,v)))
        v6-->Stat2(Stat2,Stat2*) ==> v6 in nodes(g0)
        v6-->Stat17(Stat17*) ==> Conn(filter(g0,v6))
        v6-->Stat1(Stat17*) ==> false
    Discharge ==> Stat18: AUTO
--
-- Since $HGraph(filter(g0,w0))$ is not connected, $filter(g0,w0)$ has a strict, non-null
-- subgraph $q0$ that shares no nodes with its complementary subgraph of $filter(g0,w0)$.
-- Either $q0$ or its complement must include $m0$ by Theorem hgraph13, so let $q1$ be the
-- one of these two graphs which has $m0$ as a subgraph.
--
    (g0,w0)-->Thgraph8 ==> AUTO
    Use_def(Conn(filter(g0,w0))) ==> AUTO
    w0-->Stat1(Stat9*) ==> Stat31: {p 可ncin filter(g0,w0) | nodes(p) * nodes(filter(g0,w0)-p) = 0} 叩incin {0,filter(g0,w0)}
    q0-->Stat31(Stat31*) ==> Stat32: (q0 in {p 可ncin filter(g0,w0) | nodes(p) * nodes(filter(g0,w0)-p) = 0}) & (q0 notin {0,filter(g0,w0)})
    ()-->Stat32(Stat32*) ==> Stat33: (q0 可ncin filter(g0,w0)) & (nodes(q0) * nodes(filter(g0,w0)-q0) = 0)
    (q0,filter(g0,w0),m0)-->Thgraph13(Stat9*) ==> (m0 可ncin (filter(g0,w0)-q0)) or (m0 可ncin q0)
    Loc_def ==> q1 = if m0 可ncin q0 then q0 else filter(g0,w0)-q0 end if
    (Stat32*)ELEM ==> Stat35: (q1 可ncin filter(g0,w0)) & (q1 /= filter(g0,w0)) & (m0 可ncin q1)
    Suppose ==> nodes(q1) * nodes(filter(g0,w0)-q1) /= 0
        Suppose ==> q1 = q0
        EQUAL(Stat33) ==> false; Discharge ==> AUTO
        (Stat33*)ELEM ==> (q1 = filter(g0,w0)-q0) & (q0 = filter(g0,w0)-q1) & (nodes(filter(g0,w0)-q1) * nodes(q1) /= 0)
        EQUAL(Stat33) ==> false
    Discharge ==> AUTO
--
-- Plainly $w0 notin nodes(q1)$ because $w0 notin nodes(filter(g0,w0))$. Therefore,
-- by Theorem hgraph9, we have $g0=cov(g0,q1)+cov(g0,filter(g0,w0)-q1)$. Moreover,
-- $lost(g0,w0) = 0$ holds by Theorem hgraph21, and $cov(g0,q1) * cov(g0,filter(g0,w0)-q1) = 0$
-- holds by Theorem hgraph11. It readily follows that $cov(g0,filter(g0,w0)-q1) = g0-cov(g0,q1)$.
-- Also, $nodes(cov(g0,q1)) * nodes(cov(g0,filter(g0,w0)-q1)) = {w0}$ follows from
-- Theorem hgraph12.
--
    (q1,filter(g0,w0))-->Thgraph_a(Stat18*) ==>Stat36:  w0 notin nodes(q1)
    (g0,w0,q1)-->Thgraph9 ==> AUTO
    (g0,w0)-->Thgraph21(*) ==> Stat37: (cov(g0,q1)+cov(g0,filter(g0,w0)-q1) = g0) & (lost(g0,w0) = 0) & HGraph(g0) & Conn(g0) & (w0 in nodes(g0))
    (g0,q1,w0)-->Thgraph11(Stat32*) ==> cov(g0,q1) * cov(g0,filter(g0,w0)-q1) = 0
    (Stat37*)ELEM ==> cov(g0,filter(g0,w0)-q1) = g0-cov(g0,q1)
    (g0,q1,w0)-->Thgraph12(Stat18*) ==>  nodes(cov(g0,q1)) * nodes(cov(g0,filter(g0,w0)-q1)) = {w0}
--
-- We then get $Conn(cov(g0,q1))$ by means of Theorem hgraph14.
--
    EQUAL(Stat37) ==> Conn(cov(g0,q1)+cov(g0,filter(g0,w0)-q1))
    (cov(g0,q1),cov(g0,filter(g0,w0)-q1),w0)-->Thgraph14(*) ==> Conn(cov(g0,q1))
--
-- This connected set $cov(g0,q1)$ will turn out to contradict the minimality of $m0$.
-- In the first place $cov(g0,q1)$ includes $m0$, by Theorem hgraph3, and this inclusion
-- is strict, because $w0$ belongs to the nodes of $cov(g0,q1)$ but does not belong to
-- the nodes of $m0$.
--
    (g0,q1)-->Thgraph5(Stat9*) ==> m0 可ncin cov(g0,q1)
    Suppose ==> m0 = cov(g0,q1)
        EQUAL(Stat37) ==> (w0 in nodes(m0)) 占q (w0 in nodes(cov(g0,q1)))
        (m0,q1)-->Thgraph_a(Stat35*) ==> false
    Discharge ==> AUTO
--
-- In the second place, the graph $g0-cov(g0,q1)$ (which equals $cov(g0,filter(g0,w0)-q1)$
-- as already seen, is easily shown to be non-null by means of Theorem hgraph6. 
--
    Suppose ==> Stat38: cov(g0,filter(g0,w0)-q1) = 0
        (g0,w0)-->Thgraph8 ==> AUTO
        (g0,filter(g0,w0)-q1,filter(g0,w0)-q1)-->Thgraph7(Stat38*) ==> not((nodes(g0) incs nodes(filter(g0,w0)-q1)) & HGraph(filter(g0,w0)-q1) & (filter(g0,w0)-q1 /= 0))
        Suppose ==> not HGraph(filter(g0,w0)-q1)
            (filter(g0,w0),filter(g0,w0)-q1)-->Thgraph3(Stat38*) ==> not HGraph(filter(g0,w0))
        (Stat37*)Discharge ==> AUTO
        (filter(g0,w0)-q1,filter(g0,w0))-->Thgraph_a(Stat35*) ==> false
    Discharge ==> AUTO
    (g0,g0-cov(g0,q1))-->Thgraph3(Stat37*) ==> Stat39: HGraph(g0-cov(g0,q1)) & (g0-cov(g0,q1) /= 0)
--
-- Thirdly, we can find a node $w1$ of $g0$ such that $w1/=w0$ and $w1 in nodes(g0-cov(g0,q1))$;
-- then, in view of Theorem hgraph15, we get $cov(g0,q1) 可ncin filter(g0,w1)$.
--
    e0-->Stat39(Stat39*) ==> (e0 in g0) & (e0 notin cov(g0,q1))
    (g0,e0,w0)-->Thgraph2(Stat37*) ==> Stat40: e0 叩incin {w0}
    w1-->Stat40(Stat40*) ==> (w1 in e0) & (w1 /= w0)
    (g0 - cov(g0,q1),e0,w1)-->Thgraph2(Stat39*) ==> w1 in nodes(g0 - cov(g0,q1))
    (g0,q1)-->Thgraph5(Stat37,Stat37*) ==> g0 = cov(g0,q1)+(g0-cov(g0,q1))
    EQUAL(Stat37) ==> (nodes(cov(g0,q1)) * nodes(g0-cov(g0,q1)) = {w0}) & HGraph(cov(g0,q1)+(g0-cov(g0,q1))) & (filter(cov(g0,q1)+(g0-cov(g0,q1)),w1) = filter(g0,w1))
    (cov(g0,q1),g0-cov(g0,q1),w0,w1)-->Thgraph15(Stat40*) ==> cov(g0,q1) 可ncin filter(g0,w1)
--
-- Taken together, these properties show that $cov(g0,q1)$ violates the minimality of $m0$.
-- This contradiction leads us to the desired conclusion.
--
    (cov(g0,q1))-->Stat8(Stat7,Stat7*) ==> Stat41: cov(g0,q1) notin {x in {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}-{m0} | m0 可ncin x}
    (cov(g0,q1))-->Stat41(Stat37*) ==> Stat42: cov(g0,q1) notin {p 可ncin g0 | Conn(p) & (EXISTS v in nodes(g0) | p 可ncin filter(g0,v))}
    (cov(g0,q1))-->Stat42(Stat37*) ==> Stat43: (not (EXISTS v in nodes(g0) | cov(g0,q1) 可ncin filter(g0,v)))
    (g0 - cov(g0,q1),g0)-->Thgraph_a(Stat43*) ==> nodes(g0 - cov(g0,q1)) 可ncin nodes(g0)
    w1-->Stat43(Stat40*) ==> false
Discharge ==> QED
--
-- \subsection{Cut vertices; existence of a non-cut vertex in any nonnull connected hypergraph}
--
Def hgraph8: [Disconnecting vertex] Cutting(G,V) := (G /= {edgeOf(V,G)}) & (not (Conn(filter(G,V)) & (lost(G,V) = 0)))
--
-- The following proposition corresponds to Lemma 5 of [CO14].
--
Theorem hgraph23: [A node that occurs in exactly one edge is not a cut vertex] (Conn(G) & (contains(G,V) = {E})) 可mp (not Cutting(G,V)). Proof:
Suppose_not(g0,v0,e0) ==> AUTO
    Use_def(Cutting) ==> Stat1: Conn(g0) & (g0 /= {edgeOf(v0,g0)}) & (not (Conn(filter(g0,v0)) & (lost(g0,v0) = 0))) & (contains(g0,v0)={e0})
    (g0,v0,e0)-->Thgraph20(Stat1*) ==> Stat2: lost(g0,v0) /= 0
    Use_def(Conn(g0)) ==> AUTO
    (g0,w0,v0)-->Thgraph18 ==> AUTO
    w0-->Stat2(Stat1*) ==> contains(g0,w0) = {{v0,w0}}
    Suppose ==> e0 /= {v0,w0}
        Use_def(contains) ==> Stat3: ({v0,w0} in {e : e in g0 | w0 in e}) & ({v0,w0} notin {e in g0 | v0 in e}) 
        (e1,e1)-->Stat3(Stat3*) ==> false
    Discharge ==> Stat4: e0 = {v0,w0}
    Suppose ==> cov(g0,{e0}) /= {e0}
        (g0,{e0})-->Thgraph3 ==> AUTO
        (g0,v0)-->Thgraph8(Stat1*) ==> HGraph({e0})
        ({e0},g0)-->Thgraph4(Stat4*) ==> {a: e in {e0}, v in e, a in contains(g0,v)} /= {{v0,w0}}
        SIMPLF ==> Stat5: {a: v in e0, a in contains(g0,v)} /= {{v0,w0}}
        Suppose ==> Stat6: {v0,w0} notin {a: v in e0, a in contains(g0,v)}
            (w0,{v0,w0})-->Stat6(Stat2*) ==> false 
        Discharge ==> AUTO
        w1-->Stat5(Stat5*) ==> Stat7: (w1 in {a: v in e0, a in contains(g0,v)}) & (w1 /= {v0,w0})
        (v1,u1)-->Stat7(Stat4*) ==> (v1 in {v0,w0}) & (w1 in contains(g0,v1))
        Suppose ==> v1 = v0
            EQUAL(Stat1) ==> false
        Discharge ==> v1 = w0
        EQUAL(Stat2) ==> false
    Discharge ==> AUTO
    Suppose ==> Stat8: {e0} notin {p 可ncin g0 | nodes(p) * nodes(g0-p) = 0}
        (g0,{e0})-->Thgraph6(Stat4*) ==> nodes({e0}) * nodes(g0-{e0}) = 0
        {e0}-->Stat8(*) ==> e0 notin g0
        Use_def(contains) ==> Stat9: e0 in {e in g0 | v0 in e}
        ()-->Stat9(Stat8*) ==> false
    Discharge ==> AUTO
    (Stat1*)ELEM ==> Stat11: {e0} = g0
    (v0,g0)-->Thgraph_e(Stat10*) ==> Stat10: (v0 in nodes(g0)) 可mp (edgeOf(v0,g0) in g0)
    (g0,e0)-->Thgraph2(Stat1*) ==> Stat12: e0 = edgeOf(v0,g0)
    EQUAL(Stat1,Stat11,Stat12) ==> false
    Discharge ==> QED
--
--
-- The following proof of the Corollary 1 of [CO14] also embodies the proof of the proposition named, therein, Theorem 1.
--
Theorem hgraph24: [Every non-null connected graph has a non-cut vertex] (Conn(G) & (G /= 0)) 可mp (EXISTS v in nodes(G) | not Cutting(G,v)). Proof:
Suppose_not(g0) ==> AUTO
    g0-->Thgraph22 ==> AUTO
    Use_def(Conn) ==> Stat1: (not(EXISTS v in nodes(g0) | not Cutting(g0,v))) & (EXISTS v in nodes(g0) | Conn(filter(g0,v))) & ({p 可ncin g0 | nodes(p) * nodes(g0-p) = 0} 可ncin {0,g0}) & HGraph(g0)
    Use_def(Cutting(g0,v0)) ==> AUTO 
    (v0,v0)-->Stat1(Stat1*) ==> Stat2: (lost(g0,v0) /= 0) & (v0 in nodes(g0)) & Conn(filter(g0,v0)) & (v0 in nodes(g0))
    w0-->Stat2(Stat2*) ==> w0 in lost(g0,v0) 
    Use_def(contains(g0,w0)) ==> AUTO
    (g0,w0,v0)-->Thgraph18(*) ==> Stat3: ({v0,w0} in {e in g0 | w0 in e}) & (contains(g0,w0) = {{v0,w0}})
    (g0,w0,{v0,w0})-->Thgraph23(*) ==> not Cutting(g0,w0)
    w0-->Stat1(*) ==> w0 notin nodes(g0)
    (g0,{v0,w0})-->Thgraph2(Stat1*) ==> {v0,w0} notin g0
    ()-->Stat3(Stat3*) ==> false
    Discharge ==> QED
--
--END HERE