GLENUM00

:: Introduction to Graph Enumerations
::  by Sebastian Koch
:: 
:: Received March 31, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
      FINSEQ_1, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, ORDINAL2, XXREAL_0,
      PBOOLE, GLIB_000, RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD, SCMYCIEL,
      GLIB_006, GLIB_009, GLIB_010, GLIB_012, MOD_4, RELAT_2, GRAPH_1,
      GLIB_001, ABIAN, TREES_1, EQREL_1, GLIB_013, GLIB_014, WELLORD1,
      ORDERS_1, RCOMP_1, GLIB_015, GLENUM00;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELAT_2,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, EQREL_1,
      FUNCOP_1, FUNCT_3, ORDERS_1, TOLER_1, FINSET_1, CARD_1, XCMPLX_0,
      XXREAL_0, FINSEQ_1, ABIAN, GLIB_000, GLIB_001, GLIB_002, CHORD, GLIB_006,
      GLIB_008, GLIB_009, GLIB_010, GLIB_012, GLIB_013, GLIB_014, GLIB_015;
 constructors DOMAIN_1, CHORD, GLIB_002, GLIB_008, GLIB_010, GLIB_012,
      ORDERS_1, GLIB_015, TOLER_1, COMPUT_1, EQREL_1, GLIB_013;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XREAL_0, NAT_1, FUNCT_2, RELSET_1, GLIB_000, CHORD, GLIB_002,
      GLIB_006, GLIB_009, GLIB_008, GLIB_010, XTUPLE_0, ABIAN, GLIB_001,
      MEMBERED, GLIB_012, GLIB_013, GLIB_014, GLIBPRE1, GLIB_015;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
 definitions TARSKI;
 equalities SUBSET_1, GLIB_010;
 theorems RELSET_1, GLIB_000, CHORD, GLIB_002, GLIB_006, GLIB_009, GLIB_010,
      TARSKI, ZFMISC_1, FUNCT_1, XBOOLE_0, XBOOLE_1, FUNCT_2, PARTFUN1,
      FUNCT_4, GLIB_001, RELAT_1, CARD_1, CARD_2, FUNCOP_1, XXREAL_0, GLIB_008,
      XREAL_1, ORDINAL1, GLIB_012, FINSET_1, RELAT_2, EQREL_1, BINOP_1,
      GLIBPRE0, GLIB_014, GLIB_015, ORDERS_1, MMLQUER2, WELLORD1, GLIBPRE1;
 schemes FUNCT_1, RELSET_1, GLIB_009, FUNCT_3, GLIBPRE1;

begin :: Subgraph set and Subgraph Relation

reserve G, G1, G2 for _Graph, H for Subgraph of G;

::$INSERT "SG" is short for "Subgraphs".
definition
  let G;
  func G.allSG() -> Graph-membered set equals
  { the plain inducedSubgraph of G,V,E
      where V is non empty Subset of the_Vertices_of G,
        E is Subset of the_Edges_of G
      : E c= G.edgesBetween(V) };
  coherence
  proof
    now
      let x be object;
      assume x in { the plain inducedSubgraph of G,V,E
        where V is non empty Subset of the_Vertices_of G,
          E is Subset of the_Edges_of G
        : E c= G.edgesBetween(V) };
      then consider V being non empty Subset of the_Vertices_of G,
        E being Subset of the_Edges_of G such that
        A1: x = the plain inducedSubgraph of G,V,E and
        E c= G.edgesBetween(V);
      thus x is _Graph by A1;
    end;
    hence thesis by GLIB_014:def 1;
  end;
end;

registration
  let G be _finite _Graph;
  cluster G.allSG() -> finite;
  coherence
  proof
    set V = the_Vertices_of G, E = the_Edges_of G;
    deffunc I(object,object) = the plain inducedSubgraph of G,Segm $1,Segm $2;
    consider f being Function such that
      A1: dom f = [: bool V, bool E :] and
      A2: for x,y being object st x in bool V & y in bool E
        holds f.(x,y) = I(x,y) from FUNCT_3:sch 2;
    A3: rng f is finite by A1, FINSET_1:8;
    now
      let h be object;
      assume h in G.allSG();
      then consider W being non empty Subset of the_Vertices_of G,
          F being Subset of the_Edges_of G such that
        A4: h = the plain inducedSubgraph of G,W,F & F c= G.edgesBetween(W);
      A5: Segm W = W & Segm F = F by ORDINAL1:def 17;
      f.[W,F] = f.(W,F) by BINOP_1:def 1
        .= h by A2, A4, A5;
      hence h in rng f by A1, FUNCT_1:def 3;
    end;
    then G.allSG() c= rng f by TARSKI:def 3;
    hence thesis by A3;
  end;
end;

theorem Th1:
  G2 in G1.allSG() iff G2 is plain Subgraph of G1
proof
  hereby
    assume G2 in G1.allSG();
    then consider V being non empty Subset of the_Vertices_of G1,
      E being Subset of the_Edges_of G1 such that
      A1: G2 = the plain inducedSubgraph of G1,V,E and
      E c= G1.edgesBetween(V);
    thus G2 is plain Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain Subgraph of G1;
  set G9 = the plain inducedSubgraph of G1,the_Vertices_of G2,the_Edges_of G2;
  A3: the_Vertices_of G2 c= the_Vertices_of G1 &
    the_Edges_of G2 c= the_Edges_of G1 by A2, GLIB_000:def 32;
  G2.edgesBetween(the_Vertices_of G2) c= G1.edgesBetween(the_Vertices_of G2)
    by A2, GLIB_000:76;
  then A4: the_Edges_of G2 c= G1.edgesBetween(the_Vertices_of G2)
    by GLIB_000:34;
  the_Vertices_of G9 = the_Vertices_of G2 &
    the_Edges_of G9 = the_Edges_of G2 by A3, A4, GLIB_000:def 37;
  then G9 = G2 by A2, GLIB_000:86, GLIB_009:44;
  hence thesis by A3, A4;
end;

theorem Th2:
  H | _GraphSelectors in G.allSG()
proof
  H | _GraphSelectors is Subgraph of G by GLIB_000:92, GLIB_000:128;
  hence thesis by Th1;
end;

theorem Th3:
  G | _GraphSelectors in G.allSG()
proof
  G is Subgraph of G by GLIB_000:40;
  hence thesis by Th2;
end;

Lm1:
  for V being non empty Subset of the_Vertices_of G
  for S, T being Function of {}, V
  holds createGraph(V,{},S,T) in G.allSG()
proof
  let V be non empty Subset of the_Vertices_of G;
  let S, T be Function of {}, V;
  set H = createGraph(V,{},S,T), H9 = the plain inducedSubgraph of G, V, {};
  {} c= G.edgesBetween(V) by XBOOLE_1:2;
  then A1: the_Vertices_of H9 = V & the_Edges_of H9 = {} by GLIB_000:def 37;
  A2: the_Source_of H9 = {} & the_Target_of H9 = {} by A1;
  the_Vertices_of H = V & the_Edges_of H = {} &
    the_Source_of H = S & the_Target_of H = T;
  then H = H9 by A1, A2, GLIB_000:def 34, GLIB_009:44;
  hence thesis by Th1;
end;

definition
  let G; let V be non empty Subset of the_Vertices_of G;
  func createGraph(V) -> plain Subgraph of G equals
  createGraph(V,{},the Function of {},V, the Function of {},V);
  coherence
  proof
    createGraph(V,{},the Function of {},V, the Function of {},V)
      in G.allSG() by Lm1;
    hence thesis by Th1;
  end;
end;

registration
  let G; let V be non empty Subset of the_Vertices_of G;
  cluster createGraph(V) -> edgeless;
  coherence;
end;

theorem Th4:
  for V being non empty Subset of the_Vertices_of G
  holds createGraph(V) in G.allSG() by Lm1;

theorem Th5:
  for V being non empty Subset of the_Vertices_of G
  for H being inducedSubgraph of G, V, {}
  holds H == createGraph(V)
proof
  let V be non empty Subset of the_Vertices_of G;
  let H be inducedSubgraph of G, V, {};
  {} c= G.edgesBetween(V) by XBOOLE_1:2;
  then the_Vertices_of H = the_Vertices_of createGraph(V) &
    the_Edges_of H = the_Edges_of createGraph(V) by GLIB_000:def 37;
  hence thesis by GLIB_000:86;
end;

theorem Th6:
  for H being removeEdges of G, the_Edges_of G
  holds H == createGraph([#]the_Vertices_of G)
proof
  let H be removeEdges of G, the_Edges_of G;
  the_Edges_of G \ the_Edges_of G = {} &
    [#]the_Vertices_of G = the_Vertices_of G by XBOOLE_1:37;
  hence thesis by Th5;
end;

theorem Th7:
  G is edgeless iff G == createGraph([#]the_Vertices_of G)
proof
  set H = the removeEdges of G, the_Edges_of G;
  hereby
    assume G is edgeless;
    then A1: the_Edges_of G = the_Edges_of H;
    A2: the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33;
    G is Subgraph of G by GLIB_000:40;
    then A3: G == H by A1, A2, GLIB_000:86;
    H == createGraph([#]the_Vertices_of G) by Th6;
    hence G == createGraph([#]the_Vertices_of G) by A3, GLIB_000:85;
  end;
  assume G == createGraph([#]the_Vertices_of G);
  hence thesis by GLIB_008:52;
end;

theorem Th8:
  for V being non empty Subset of the_Vertices_of G1
  st V c= the_Vertices_of G2 holds createGraph(V) is Subgraph of G2
proof
  let V be non empty Subset of the_Vertices_of G1;
  assume A1: V c= the_Vertices_of G2;
  for e being set st e in the_Edges_of createGraph(V) holds
    (the_Source_of createGraph(V)).e = (the_Source_of G2).e &
    (the_Target_of createGraph(V)).e = (the_Target_of G2).e;
  hence thesis by A1, XBOOLE_1:2, GLIB_000:def 32;
end;

theorem Th9:
  G is edgeless iff G.allSG() = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G
proof
  set S = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G;
  hereby
    assume A1: G is edgeless;
    now
      let x be object;
      hereby
        assume x in G.allSG();
        then reconsider H = x as plain Subgraph of G by Th1;
        reconsider V = [#]the_Vertices_of H
          as non empty Subset of the_Vertices_of G;
        H == createGraph([#]the_Vertices_of H) by A1, Th7;
        then H = createGraph(V) by GLIB_009:44;
        hence x in S;
      end;
      assume x in S;
      then consider V being non empty Subset of the_Vertices_of G such that
        A2: x = createGraph(V);
      thus x in G.allSG() by A2, Th4;
    end;
    hence G.allSG() = S by TARSKI:2;
  end;
  assume G.allSG() = S;
  then G | _GraphSelectors in S by Th3;
  then consider V being non empty Subset of the_Vertices_of G such that
    A3: G | _GraphSelectors = createGraph(V);
  G == G | _GraphSelectors by GLIB_000:128;
  hence G is edgeless by A3, GLIB_008:52;
end;

Lm2:
  for v being Vertex of G, S, T being Function of {}, {v}
  holds createGraph({v},{},S,T) in G.allSG() by Lm1;

definition
  let G; let v be Vertex of G;
  func createGraph(v) -> plain Subgraph of G equals
  createGraph({v});
  coherence;
end;

registration
  let G; let v be Vertex of G;
  cluster createGraph(v) -> _trivial edgeless;
  coherence;
end;

theorem
  for v being Vertex of G holds createGraph(v) in G.allSG() by Lm2;

theorem
  for v being Vertex of G, H being inducedSubgraph of G, {v}, {}
  holds H == createGraph(v) by Th5;

theorem
  for v being Vertex of G1 st v in the_Vertices_of G2
  holds createGraph(v) is Subgraph of G2 by Th8, ZFMISC_1:31;

definition
  let G be non edgeless _Graph, e be Edge of G;
  func createGraph(e) -> plain Subgraph of G means
  :Def4:
  ex V being non empty Subset of the_Vertices_of G,
    S, T being Function of {e}, V
  st it = createGraph(V,{e},S,T) &
    {(the_Source_of G).e,(the_Target_of G).e} = V &
    S = e .--> (the_Source_of G).e & T = e .--> (the_Target_of G).e;
  existence
  proof
    set v = (the_Source_of G).e, w = (the_Target_of G).e;
    reconsider V = {v,w} as non empty Subset of the_Vertices_of G;
    set S = e .--> v, T = e .--> w;
    dom S = dom{[e,v]} & dom T = dom{[e,w]} by FUNCT_4:82;
    then A1: dom S = {e} & dom T = {e} by RELAT_1:9;
    rng S = {v} & rng T = {w} by FUNCOP_1:88;
    then reconsider S, T as Function of {e},V by A1, ZFMISC_1:7, FUNCT_2:2;
    set H = createGraph(V,{e},S,T);
    now
      thus the_Vertices_of H c= the_Vertices_of G &
        the_Edges_of H c= the_Edges_of G;
      let e0 be set;
      assume e0 in the_Edges_of H;
      then A2: e0 = e by TARSKI:def 1;
      thus (the_Source_of H).e0 = (the_Source_of G).e0 by A2, FUNCOP_1:72;
      thus (the_Target_of H).e0 = (the_Target_of G).e0 by A2, FUNCOP_1:72;
    end;
    then reconsider H as plain Subgraph of G by GLIB_000:def 32;
    take H,V,S,T;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th13:
  for G being non edgeless _Graph, e being Edge of G
  holds the_Edges_of createGraph(e) = {e} & the_Vertices_of createGraph(e)
    = {(the_Source_of G).e,(the_Target_of G).e}
proof
  let G be non edgeless _Graph, e be Edge of G;
  consider V being non empty Subset of the_Vertices_of G,
    S, T being Function of {e}, V such that
    A1: createGraph(e) = createGraph(V,{e},S,T) &
      {(the_Source_of G).e,(the_Target_of G).e} = V &
      S = e .--> (the_Source_of G).e & T = e .--> (the_Target_of G).e
    by Def4;
  thus thesis by A1;
end;

theorem Th14:
  for G being non edgeless _Graph, e being Edge of G
  holds e DJoins (the_Source_of G).e,(the_Target_of G).e,createGraph(e)
proof
  let G be non edgeless _Graph, e be Edge of G;
  A1: e DJoins (the_Source_of G).e,(the_Target_of G).e,G by GLIB_000:def 14;
  the_Edges_of createGraph(e) = {e} by Th13;
  then e in the_Edges_of createGraph(e) by TARSKI:def 1;
  hence thesis by A1, GLIB_000:73;
end;

theorem Th15:
  for G being non edgeless _Graph, e being Edge of G, e0,v,w being object
  st e0 DJoins v,w,createGraph(e)
  holds e0 = e & v = (the_Source_of G).e & w = (the_Target_of G).e
proof
  let G be non edgeless _Graph, e be Edge of G, e0,v,w be object;
  assume A1: e0 DJoins v,w,createGraph(e);
  then e0 in the_Edges_of createGraph(e) by GLIB_000:def 14;
  then e0 in {e} by Th13;
  then A2: e0 = e & v is set & w is set by TARSKI:def 1, TARSKI:1;
  then e DJoins v,w,G by A1, GLIB_000:72;
  hence thesis by A2, GLIB_000:def 14;
end;

theorem Th16:
  for G being non edgeless _Graph, e being Edge of G, e0,v,w being object
  st e0 Joins v,w,createGraph(e) holds e0 = e
proof
  let G be non edgeless _Graph, e be Edge of G, e0,v,w be object;
  assume e0 Joins v,w,createGraph(e);
  then e0 DJoins v,w,createGraph(e) or e0 DJoins w,v,createGraph(e)
    by GLIB_000:16;
  hence thesis by Th15;
end;

registration
  let G be non edgeless _Graph, e be Edge of G;
  cluster createGraph(e) -> non edgeless non-multi connected _finite;
  coherence
  proof
    the_Edges_of createGraph(e) = {e} by Th13;
    hence createGraph(e) is non edgeless;
    now
      let e1,e2,v1,v2 be object;
      assume e1 Joins v1,v2,createGraph(e) & e2 Joins v1,v2,createGraph(e);
      then e1 in the_Edges_of createGraph(e) &
        e2 in the_Edges_of createGraph(e) by GLIB_000:def 13;
      then e1 in {e} & e2 in {e} by Th13;
      then e1 = e & e2 = e by TARSKI:def 1;
      hence e1 = e2;
    end;
    hence createGraph(e) is non-multi by GLIB_000:def 20;
    set v = (the_Source_of G).e, w = (the_Target_of G).e;
    for x,y being Vertex of createGraph(e) ex W being Walk of createGraph(e)
      st W is_Walk_from x,y
    proof
      let x,y be Vertex of createGraph(e);
      per cases;
      suppose x = y;
        then (createGraph(e)).walkOf(x) is_Walk_from x,y by GLIB_001:13;
        hence thesis;
      end;
      suppose A1: x <> y;
        e DJoins v,w,createGraph(e) by Th14;
        then A2: e Joins v,w,createGraph(e) & e Joins w,v,createGraph(e)
          by GLIB_000:16;
        the_Vertices_of createGraph(e) = {v,w} by Th13;
        then ((x=v or x=w)&(y=v or y=w)) by TARSKI:def 2;
        then per cases by A1;
        suppose x = v & y = w;
          then (createGraph(e)).walkOf(v,e,w) is_Walk_from x,y
            by A2, GLIB_001:15;
          hence thesis;
        end;
        suppose x = w & y = v;
          then (createGraph(e)).walkOf(w,e,v) is_Walk_from x,y
            by A2, GLIB_001:15;
          hence thesis;
        end;
      end;
    end;
    hence createGraph(e) is connected by GLIB_002:def 1;
    the_Vertices_of createGraph(e) = {v,w} & the_Edges_of createGraph(e) = {e}
      by Th13;
    hence createGraph(e) is _finite by GLIB_000:def 17;
  end;
end;

theorem Th17:
  for G being non edgeless _Graph, e being Edge of G
  holds createGraph(e) is loopless iff not e in G.loops()
proof
  let G be non edgeless _Graph, e be Edge of G;
  hereby
    assume A1: createGraph(e) is loopless;
    assume e in G.loops();
    then consider v being object such that
      A2: e Joins v,v,G by GLIB_009:def 2;
    (the_Source_of G).e = v & (the_Target_of G).e = v by A2, GLIB_000: def 13;
    hence contradiction by A1, Th14, GLIB_000:136;
  end;
  assume A3: not e in G.loops();
  assume not createGraph(e) is loopless;
  then consider v,e0 being object such that
    A4: e0 DJoins v,v,createGraph(e) by GLIB_000:136;
  e0 = e & v is set by A4, Th15, TARSKI:1;
  hence contradiction by A3, A4, GLIB_000:72, GLIB_009:45;
end;

theorem Th18:
  for G being non edgeless _Graph, e being Edge of G
  holds createGraph(e) is acyclic iff not e in G.loops()
proof
  let G be non edgeless _Graph, e be Edge of G;
  thus createGraph(e) is acyclic implies not e in G.loops() by Th17;
  assume A1: not e in G.loops();
  assume createGraph(e) is non acyclic;
  then consider W2 being Walk of createGraph(e) such that
    A2: W2 is Cycle-like by GLIB_002:def 2;
  A3: len W2.vertexSeq() <= (createGraph(e)).order() + 1 by A2, GLIB_001:154;
  set v = (the_Source_of G).e, w = (the_Target_of G).e;
  A4: the_Vertices_of createGraph(e) = {v,w} by Th13;
  card {v,w} <= 2 by CARD_2:50;
  then (createGraph(e)).order() <= 2 by A4, GLIB_000:def 24;
  then (createGraph(e)).order() + 1 <= 2+1 by XREAL_1:6;
  then len W2.vertexSeq() <= 2+1 by A3, XXREAL_0:2;
  then len W2.vertexSeq() = 0 or ... or len W2.vertexSeq() = 3;
  then per cases;
  suppose len W2.vertexSeq() = 0;
    hence contradiction by GLIB_001:67;
  end;
  suppose len W2.vertexSeq() = 1;
    then W2.length() + 1 = 0 + 1 by GLIB_009:28;
    hence contradiction by A2, GLIB_001:def 26;
  end;
  suppose len W2.vertexSeq() = 2;
    then W2.length() + 1 = 1 + 1 by GLIB_009:28;
    then A5: len W2 = 2*1+1 by GLIB_001:112;
    then 1 is odd & 1 < len W2;
    then A6: W2.(1+1) Joins W2.1,W2.(1+2),createGraph(e) by GLIB_001:def 3;
    W2.1 = W2.first() by GLIB_001:def 6
      .= W2.last() by A2, GLIB_001:def 24
      .= W2.3 by A5, GLIB_001:def 7;
    then e Joins W2.1,W2.1,createGraph(e) by A6, Th16;
    then e in (createGraph(e)).loops() by GLIB_009:def 2;
    hence contradiction by A1, GLIB_009:48, TARSKI:def 3;
  end;
  suppose len W2.vertexSeq() = 3;
    then W2.length() + 1 = 2 + 1 by GLIB_009:28;
    then len W2.edgeSeq() = 2 by GLIB_001:def 18;
    then A7: 2 <= (createGraph(e)).size() by A2, GLIB_001:144;
    the_Edges_of createGraph(e) = {e} by Th13;
    then card the_Edges_of createGraph(e) = 1 by CARD_1:30;
    then (createGraph(e)).size() = 1 by GLIB_000:def 25;
    hence contradiction by A7;
  end;
end;

theorem
  for G being non edgeless _Graph, e being Edge of G
  holds createGraph(e) in G.allSG() by Th1;

theorem
  for G being non edgeless _Graph, e being Edge of G, H being
    inducedSubgraph of G, {(the_Source_of G).e, (the_Target_of G).e}, {e}
  holds H == createGraph(e)
proof
  let G be non edgeless _Graph, e being Edge of G;
  set V = {(the_Source_of G).e, (the_Target_of G).e};
  let H be inducedSubgraph of G, V, {e};
  (the_Source_of G).e in V & (the_Target_of G).e in V by TARSKI:def 2;
  then A1: {e} c= G.edgesBetween(V) by ZFMISC_1:31, GLIB_000:31;
  the_Vertices_of H = V & the_Edges_of H = {e} by A1, GLIB_000:def 37;
  then the_Vertices_of H = the_Vertices_of createGraph(e) &
    the_Edges_of H = the_Edges_of createGraph(e) by Th13;
  hence thesis by GLIB_000:86;
end;

theorem Th21:
  for G being non edgeless _Graph, e being Edge of G
  for V being Subset of the_Vertices_of G
  for H being addVertices of createGraph(e), V
  holds H is Subgraph of G
proof
  let G be non edgeless _Graph, e be Edge of G;
  let V be Subset of the_Vertices_of G;
  let H be addVertices of createGraph(e), V;
  the_Vertices_of H = the_Vertices_of createGraph(e) \/ V by GLIB_006:def 10;
  then A1: the_Vertices_of H c= the_Vertices_of G;
  the_Edges_of H = the_Edges_of createGraph(e) by GLIB_006:def 10;
  then A2: the_Edges_of H c= the_Edges_of G;
  now
    let e0 be set;
    assume e0 in the_Edges_of H;
    then A3: e0 in the_Edges_of createGraph(e) by GLIB_006:def 10;
    thus (the_Source_of H).e0
       = (the_Source_of createGraph(e)).e0 by GLIB_006:def 10
      .= (the_Source_of G).e0 by A3, GLIB_000:def 32;
    thus (the_Target_of H).e0
       = (the_Target_of createGraph(e)).e0 by GLIB_006:def 10
      .= (the_Target_of G).e0 by A3, GLIB_000:def 32;
  end;
  hence thesis by A1, A2, GLIB_000:def 32;
end;

theorem Th22:
  for G being edgeless _Graph, S being GraphUnionSet, G9 being GraphUnion of S
  st (for v being Vertex of G ex H9 being Element of S st
      v in the_Vertices_of H9)
  holds G is Subgraph of G9
proof
  let G be edgeless _Graph, S be GraphUnionSet, G9 be GraphUnion of S;
  assume A1: for v being Vertex of G ex H9 being Element of S st
    v in the_Vertices_of H9;
  now
    let x be object;
    assume x in the_Vertices_of G;
    then consider H9 being Element of S such that
      A2: x in the_Vertices_of H9 by A1;
    H9 is Subgraph of G9 by GLIB_014:21;
    then the_Vertices_of H9 c= the_Vertices_of G9 by GLIB_000:def 32;
    hence x in the_Vertices_of G9 by A2;
  end;
  hence thesis by TARSKI:def 3, GLIBPRE1:68;
end;

theorem Th23:
  for G being non edgeless _Graph, S being GraphUnionSet
  for G9 being GraphUnion of S
  st (for v being Vertex of G ex H9 being Element of S st
      v in the_Vertices_of H9) &
    (for e being Edge of G ex H9 being Element of S st
      createGraph(e) is Subgraph of H9)
  holds G is Subgraph of G9
proof
  let G be non edgeless _Graph, S be GraphUnionSet;
  let G9 be GraphUnion of S;
  assume that
    A1: for v being Vertex of G ex H9 being Element of S st
      v in the_Vertices_of H9 and
    A2: for e being Edge of G ex H9 being Element of S st
      createGraph(e) is Subgraph of H9;
  now
    let x be object;
    assume x in the_Vertices_of G;
    then consider H9 being Element of S such that
      A3: x in the_Vertices_of H9 by A1;
    H9 is Subgraph of G9 by GLIB_014:21;
    then the_Vertices_of H9 c= the_Vertices_of G9 by GLIB_000:def 32;
    hence x in the_Vertices_of G9 by A3;
  end;
  then A4: the_Vertices_of G c= the_Vertices_of G9 by TARSKI:def 3;
  now
    let x be object;
    assume x in the_Edges_of G;
    then reconsider e = x as Edge of G;
    consider H9 being Element of S such that
      A5: createGraph(e) is Subgraph of H9 by A2;
    H9 is Subgraph of G9 by GLIB_014:21;
    then createGraph(e) is Subgraph of G9 by A5, GLIB_000:43;
    then the_Edges_of createGraph(e) c= the_Edges_of G9 by GLIB_000:def 32;
    then {e} c= the_Edges_of G9 by Th13;
    hence x in the_Edges_of G9 by ZFMISC_1:31;
  end;
  then A6: the_Edges_of G c= the_Edges_of G9 by TARSKI:def 3;
  now
    let e0 be set;
    assume e0 in the_Edges_of G;
    then reconsider e = e0 as Edge of G;
    consider H9 being Element of S such that
      A7: createGraph(e) is Subgraph of H9 by A2;
    H9 is Subgraph of G9 by GLIB_014:21;
    then A8: createGraph(e) is Subgraph of G9 by A7, GLIB_000:43;
    the_Edges_of createGraph(e) = {e} by Th13;
    then A9: e0 in the_Edges_of createGraph(e) by TARSKI:def 1;
    then (the_Source_of createGraph(e)).e0 = (the_Source_of G9).e0 &
      (the_Target_of createGraph(e)).e0 = (the_Target_of G9).e0
      by A8, GLIB_000:def 32;
    hence (the_Source_of G).e0 = (the_Source_of G9).e0 &
      (the_Target_of G).e0 = (the_Target_of G9).e0 by A9, GLIB_000:def 32;
  end;
  hence thesis by A4, A6, GLIB_000:def 32;
end;

theorem Th24:
  for G being edgeless _Graph, S being GraphUnionSet, G9 being GraphUnion of S
  st (for v being Vertex of G holds createGraph(v) in S)
  holds G is Subgraph of G9
proof
  let G be edgeless _Graph, S be GraphUnionSet, G9 be GraphUnion of S;
  assume A1: for v being Vertex of G holds createGraph(v) in S;
  now
    let v be Vertex of G;
    reconsider H9 = createGraph(v) as Element of S by A1;
    take H9;
    thus v in the_Vertices_of H9 by TARSKI:def 1;
  end;
  hence thesis by Th22;
end;

theorem Th25:
  for G being non edgeless _Graph, S being GraphUnionSet
  for G9 being GraphUnion of S
  st (for v being Vertex of G holds createGraph(v) in S) &
    (for e being Edge of G holds createGraph(e) in S)
  holds G is Subgraph of G9
proof
  let G be non edgeless _Graph, S be GraphUnionSet, G9 be GraphUnion of S;
  assume that
    A1: for v being Vertex of G holds createGraph(v) in S and
    A2: for e being Edge of G holds createGraph(e) in S;
  A3: now
    let v be Vertex of G;
    reconsider H9 = createGraph(v) as Element of S by A1;
    take H9;
    thus v in the_Vertices_of H9 by ZFMISC_1:31;
  end;
  now
    let e be Edge of G;
    reconsider H9 = createGraph(e) as Element of S by A2;
    take H9;
    thus createGraph(e) is Subgraph of H9 by GLIB_000:40;
  end;
  hence thesis by A3, Th23;
end;

theorem Th26:
  for G being non edgeless _Graph, E being set, e being Edge of G
  for H being removeEdges of G, E st not e in E
  holds createGraph(e) is Subgraph of H
proof
  let G be non edgeless _Graph, E being set, e being Edge of G;
  let H be removeEdges of G, E;
  assume A1: not e in E;
  the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33;
  then A2: the_Vertices_of createGraph(e) c= the_Vertices_of H;
  the_Edges_of H = the_Edges_of G \ E by GLIB_000:53;
  then e in the_Edges_of H by A1, XBOOLE_0:def 5;
  then {e} c= the_Edges_of H by ZFMISC_1:31;
  then the_Edges_of createGraph(e) c= the_Edges_of H by Th13;
  hence thesis by A2, GLIB_000:44;
end;

theorem Th27:
  for G being non edgeless _Graph, H being removeLoops of G
  for S being GraphUnionSet, G9 being GraphUnion of S
  st (for v being Vertex of G ex H9 being Element of S st
      v in the_Vertices_of H9) &
    (for e being Edge of G st not e in G.loops() ex H9 being Element of S st
      createGraph(e) is Subgraph of H9)
  holds H is Subgraph of G9
proof
  let G be non edgeless _Graph, H being removeLoops of G;
  let S be GraphUnionSet, G9 be GraphUnion of S;
  assume that
    A1: for v being Vertex of G ex H9 being Element of S st
      v in the_Vertices_of H9 and
    A2: for e being Edge of G st not e in G.loops() ex H9 being Element of S st
      createGraph(e) is Subgraph of H9;
  now
    let x be object;
    assume x in the_Vertices_of H;
    then consider H9 being Element of S such that
      A3: x in the_Vertices_of H9 by A1;
    H9 is Subgraph of G9 by GLIB_014:21;
    then the_Vertices_of H9 c= the_Vertices_of G9 by GLIB_000:def 32;
    hence x in the_Vertices_of G9 by A3;
  end;
  then A4: the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;
  now
    let x be object;
    assume x in the_Edges_of H;
    then x in the_Edges_of G \ G.loops() by GLIB_000:53;
    then A5: x in the_Edges_of G & not x in G.loops() by XBOOLE_0:def 5;
    then reconsider e = x as Edge of G;
    consider H9 being Element of S such that
      A6: createGraph(e) is Subgraph of H9 by A2, A5;
    H9 is Subgraph of G9 by GLIB_014:21;
    then createGraph(e) is Subgraph of G9 by A6, GLIB_000:43;
    then the_Edges_of createGraph(e) c= the_Edges_of G9 by GLIB_000:def 32;
    then {e} c= the_Edges_of G9 by Th13;
    hence x in the_Edges_of G9 by ZFMISC_1:31;
  end;
  then A7: the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;
  now
    let e0 be set;
    assume e0 in the_Edges_of H;
    then e0 in the_Edges_of G \ G.loops() by GLIB_000:53;
    then A8: e0 in the_Edges_of G & not e0 in G.loops() by XBOOLE_0:def 5;
    then reconsider e = e0 as Edge of G;
    consider H9 being Element of S such that
      A9: createGraph(e) is Subgraph of H9 by A2, A8;
    H9 is Subgraph of G9 by GLIB_014:21;
    then A10: createGraph(e) is Subgraph of G9 by A9, GLIB_000:43;
    the_Edges_of createGraph(e) = {e} by Th13;
    then A11: e0 in the_Edges_of createGraph(e) by TARSKI:def 1;
    then A12: (the_Source_of createGraph(e)).e0 = (the_Source_of G9).e0 &
      (the_Target_of createGraph(e)).e0 = (the_Target_of G9).e0
      by A10, GLIB_000:def 32;
    createGraph(e) is Subgraph of H by A8, Th26;
    hence (the_Source_of H).e0 = (the_Source_of G9).e0 &
      (the_Target_of H).e0 = (the_Target_of G9).e0 by A11, A12
, GLIB_000:def 32;
  end;
  hence thesis by A4, A7, GLIB_000:def 32;
end;

theorem
  for G being non edgeless _Graph, H being removeLoops of G
  for S being GraphUnionSet, G9 being GraphUnion of S
  st (for v being Vertex of G holds createGraph(v) in S) &
    (for e being Edge of G st not e in G.loops() holds createGraph(e) in S)
  holds H is Subgraph of G9
proof
  let G be non edgeless _Graph, H being removeLoops of G;
  let S be GraphUnionSet, G9 be GraphUnion of S;
  assume that
    A1: for v being Vertex of G holds createGraph(v) in S and
    A2: for e being Edge of G st not e in G.loops() holds createGraph(e) in S;
  A3: now
    let v be Vertex of G;
    reconsider H9 = createGraph(v) as Element of S by A1;
    take H9;
    thus v in the_Vertices_of H9 by ZFMISC_1:31;
  end;
  now
    let e be Edge of G;
    assume not e in G.loops();
    then reconsider H9 = createGraph(e) as Element of S by A2;
    take H9;
    thus createGraph(e) is Subgraph of H9 by GLIB_000:40;
  end;
  hence thesis by A3, Th27;
end;

registration
  let G;
  cluster G.allSG() -> non empty \/-tolerating plain;
  coherence
  proof
    thus G.allSG() is non empty by Th3;
    now
      let H1, H2 be _Graph;
      assume H1 in G.allSG() & H2 in G.allSG();
      then H1 is Subgraph of G & H2 is Subgraph of G by Th1;
      hence H1 tolerates H2 by GLIB_014:14;
    end;
    hence G.allSG() is \/-tolerating by GLIB_014:def 23;
    for H being _Graph st H in G.allSG() holds H is plain by Th1;
    hence G.allSG() is plain by GLIB_014:def 2;
  end;
end;

definition
  let G; let S be non empty Subset of G.allSG();
  redefine mode Element of S -> Subgraph of G;  :: redefines Element (SUBSET_1, definition)
  coherence
  proof
    let H be Element of S;
    thus thesis by Th1;
  end;
end;

theorem Th29:
  G2.allSG() c= G1.allSG() iff G2 is Subgraph of G1
proof
  hereby
    assume A1: G2.allSG() c= G1.allSG();
    G2 | _GraphSelectors in G2.allSG() by Th3;
    then A2: G2 | _GraphSelectors is Subgraph of G1 by A1, Th1;
    G2 == G2 | _GraphSelectors by GLIB_000:128;
    hence G2 is Subgraph of G1 by A2, GLIB_000:92;
  end;
  assume A3: G2 is Subgraph of G1;
  now
    let x be object;
    assume A4: x in G2.allSG();
    then reconsider H = x as _Graph;
    H is Subgraph of G2 by A4, Th1;
    then H is Subgraph of G1 by A3, GLIB_000:43;
    hence x in G1.allSG() by A4, Th1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  G1 == G2 iff G1.allSG() = G2.allSG()
proof
  hereby
    assume G1 == G2;
    then G1 is Subgraph of G2 & G2 is Subgraph of G1 by GLIB_000:87;
    then G2.allSG() c= G1.allSG() &
      G1.allSG() c= G2.allSG() by Th29;
    hence G1.allSG() = G2.allSG() by XBOOLE_0:def 10;
  end;
  assume G1.allSG() = G2.allSG();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th29;
  hence G1 == G2 by GLIB_000:87;
end;

definition
  let G1, G2; let F be PGraphMapping of G1, G2;
  func SG2SGFunc(F) -> Function of G1.allSG(), G2.allSG() means
  :Def5:
  for H being plain Subgraph of G1 holds it.H = rng(F | H);
  existence
  proof
    deffunc A(Element of [#]G1.allSG()) = rng(F | $1);
    A1: for x being Element of [#]G1.allSG()
      holds A(x) in G2.allSG() by Th1;
    consider f being Function of [#]G1.allSG(), G2.allSG() such that
      A2: for H being Element of [#]G1.allSG() holds f.H = A(H)
      from GLIBPRE1:sch 1(A1);
    reconsider f as Function of G1.allSG(), G2.allSG();
    take f;
    let H be plain Subgraph of G1;
    H is Element of [#]G1.allSG() by Th1;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f1, f2 be Function of G1.allSG(), G2.allSG();
    assume that
      A3: for H being plain Subgraph of G1 holds f1.H = rng(F | H) and
      A4: for H being plain Subgraph of G1 holds f2.H = rng(F | H);
    now
      let x be object;
      assume x in G1.allSG();
      then reconsider H = x as plain Subgraph of G1 by Th1;
      thus f1.x = rng(F | H) by A3
        .= f2.x by A4;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

registration
  let G1, G2; let F be PGraphMapping of G1, G2;
  cluster SG2SGFunc(F) -> non empty Graph-yielding;
  coherence
  proof
    thus SG2SGFunc(F) is non empty;
    now
      let x be object;
      assume x in dom SG2SGFunc(F);
      then reconsider H = x as plain Subgraph of G1 by Th1;
      SG2SGFunc(F).H = rng(F | H) by Def5;
      hence SG2SGFunc(F).x is _Graph;
    end;
    hence thesis by GLIB_000:def 53;
  end;
  cluster dom SG2SGFunc(F) -> Graph-membered;
  coherence;
end;

registration
  let G1, G2; let F be PGraphMapping of G1, G2;
  cluster dom SG2SGFunc(F) -> plain;
  coherence;
end;

theorem Th31:
  for F being PGraphMapping of G1, G2
  st F is weak_SG-embedding holds SG2SGFunc(F) is one-to-one
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is weak_SG-embedding;
  now
    let x1,x2 be object;
    set f = SG2SGFunc(F);
    assume A2: x1 in dom f & x2 in dom f & f.x1 = f.x2;
    then reconsider H1 = x1, H2 = x2 as plain Subgraph of G1 by Th1;
    A3: rng(F | H1) = f.x1 by Def5
      .= rng(F | H2) by A2, Def5;
    A4: F | H1 is total & F | H2 is total by A1, GLIB_010:57;
    A5: F_V.:the_Vertices_of H1
       = rng(F_V | the_Vertices_of H1) by RELAT_1:115
      .= the_Vertices_of rng(F | H1) by A4, GLIB_010:54
      .= rng(F|H2)_V by A3, A4, GLIB_010:54
      .= F_V.:the_Vertices_of H2 by RELAT_1:115;
    the_Vertices_of H1 c= the_Vertices_of G1 &
      the_Vertices_of H2 c= the_Vertices_of G1;
    then the_Vertices_of H1 c= dom F_V & the_Vertices_of H2 c= dom F_V
      by A1, GLIB_010:def 11;
    then A6: the_Vertices_of H1 c= the_Vertices_of H2 &
      the_Vertices_of H2 c= the_Vertices_of H1 by A1, A5, FUNCT_1:87;
    A7: F_E.:the_Edges_of H1
       = rng(F_E | the_Edges_of H1) by RELAT_1:115
      .= the_Edges_of rng(F | H1) by A4, GLIB_010:54
      .= rng(F|H2)_E by A3, A4, GLIB_010:54
      .= F_E.:the_Edges_of H2 by RELAT_1:115;
    the_Edges_of H1 c= the_Edges_of G1 &
      the_Edges_of H2 c= the_Edges_of G1;
    then the_Edges_of H1 c= dom F_E & the_Edges_of H2 c= dom F_E
      by A1, GLIB_010:def 11;
    then the_Edges_of H1 c= the_Edges_of H2 &
      the_Edges_of H2 c= the_Edges_of H1 by A1, A7, FUNCT_1:87;
    then H1 is Subgraph of H2 & H2 is Subgraph of H1 by A6, GLIB_000:44;
    hence x1 = x2 by GLIB_000:87, GLIB_009:44;
  end;
  hence thesis by FUNCT_1:def 4;
end;

registration
  let G1 be _Graph, G2 be G1-isomorphic _Graph, F be Isomorphism of G1, G2;
  cluster SG2SGFunc(F) -> one-to-one;
  coherence by Th31;
end;

theorem Th32:
  for F being PGraphMapping of G1, G2 st F is onto
  holds rng SG2SGFunc(F) = G2.allSG()
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is onto;
  now
    let x be object;
    assume x in G2.allSG();
    then reconsider H2 = x as plain Subgraph of G2 by Th1;
    set H1 = the plain inducedSubgraph of
      G1, F_V"the_Vertices_of H2, F_E"the_Edges_of H2;
    H1 in G1.allSG() by Th1;
    then A2: H1 in dom SG2SGFunc(F) by FUNCT_2:def 1;
    rng F == G2 by A1, GLIB_010:56;
    then H2 is Subgraph of rng F by GLIB_000:91;
    then H2 = rng(F | H1) by A1, GLIB_009:44, GLIBPRE1:99
      .= SG2SGFunc(F).H1 by Def5;
    hence x in rng SG2SGFunc(F) by A2, FUNCT_1:def 3;
  end;
  then G2.allSG() c= rng SG2SGFunc(F) by TARSKI:def 3;
  hence thesis by XBOOLE_0:def 10;
end;

:: the other direction doesn't hold for all graphs, but for finite ones
:: which is not proven here
theorem
  G2 is G1-Disomorphic implies G1.allSG(),G2.allSG() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  A2: dom SG2SGFunc F = G1.allSG() by FUNCT_2:def 1;
  A3: rng SG2SGFunc F = G2.allSG() by A1, Th32;
  A4: SG2SGFunc F is one-to-one by A1, Th31;
  now
    let G be _Graph;
    assume G in G1.allSG();
    then reconsider H = G as plain Subgraph of G1 by Th1;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A5: (SG2SGFunc F).G = rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence (SG2SGFunc F).G is G-Disomorphic _Graph
      by A5, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem
  G2 is G1-isomorphic implies G1.allSG(),G2.allSG() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  A2: dom SG2SGFunc F = G1.allSG() by FUNCT_2:def 1;
  A3: rng SG2SGFunc F = G2.allSG() by A1, Th32;
  A4: SG2SGFunc F is one-to-one by A1, Th31;
  now
    let G be _Graph;
    assume G in G1.allSG();
    then reconsider H = G as plain Subgraph of G1 by Th1;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A5: (SG2SGFunc F).G = rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence (SG2SGFunc F).G is G-isomorphic _Graph
      by A5, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem Th35:
  G is GraphUnion of G.allSG()
proof
  set G9 = the GraphUnion of G.allSG();
  set G8 = the GraphUnion of {G};
  G | _GraphSelectors in G.allSG() by Th3;
  then A1: G | _GraphSelectors is Subgraph of G9 by GLIB_014:21;
  G == G | _GraphSelectors by GLIB_000:128;
  then A2: G is Subgraph of G9 by A1, GLIB_000:92;
  now
    let H2 be Element of G.allSG();
    reconsider H1 = G as Element of {G} by TARSKI:def 1;
    take H1;
    thus H2 is Subgraph of H1 by Th1;
  end;
  then G9 is Subgraph of G8 by GLIBPRE1:118;
  then G9 is Subgraph of G by GLIB_000:91, GLIB_014:24;
  hence thesis by A2, GLIB_000:87, GLIB_014:22;
end;

theorem Th36:
  (G is loopless iff G.allSG() is loopless) &
  (G is non-multi iff G.allSG() is non-multi) &
  (G is non-Dmulti iff G.allSG() is non-Dmulti) &
  (G is simple iff G.allSG() is simple) &
  (G is Dsimple iff G.allSG() is Dsimple) &
  (G is acyclic iff G.allSG() is acyclic) &
  (G is edgeless iff G.allSG() is edgeless)
proof
  :: loopless
  thus A1: G is loopless implies G.allSG() is loopless
  proof
    assume A2: G is loopless;
    G is GraphUnion of G.allSG() by Th35;
    hence G.allSG() is loopless by A2, GLIB_014:23;
  end;
  thus A3: G.allSG() is loopless implies G is loopless
  proof
    assume A4: G.allSG() is loopless;
    G is GraphUnion of G.allSG() by Th35;
    hence G is loopless by A4;
  end;
  :: non-multi
  thus A5: G is non-multi implies G.allSG() is non-multi
  proof
    assume A6: G is non-multi;
    now
      let H be _Graph;
      assume H in G.allSG();
      then H is Subgraph of G by Th1;
      hence H is non-multi by A6;
    end;
    hence thesis by GLIB_014:def 4;
  end;
  thus A7: G.allSG() is non-multi implies G is non-multi
  proof
    assume A8: G.allSG() is non-multi;
    G | _GraphSelectors in G.allSG() by Th3;
    then A9: G | _GraphSelectors is non-multi by A8;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A9, GLIB_000:89;
  end;
  :: non-Dmulti
  thus A10: G is non-Dmulti implies G.allSG() is non-Dmulti
  proof
    assume A11: G is non-Dmulti;
    now
      let H be _Graph;
      assume H in G.allSG();
      then H is Subgraph of G by Th1;
      hence H is non-Dmulti by A11;
    end;
    hence thesis by GLIB_014:def 5;
  end;
  thus A12: G.allSG() is non-Dmulti implies G is non-Dmulti
  proof
    assume A13: G.allSG() is non-Dmulti;
    G | _GraphSelectors in G.allSG() by Th3;
    then A14: G | _GraphSelectors is non-Dmulti by A13;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A14, GLIB_000:89;
  end;
  :: simple
  thus G is simple implies G.allSG() is simple by A1, A5;
  thus G.allSG() is simple implies G is simple by A3, A7;
  :: Dsimple
  thus G is Dsimple implies G.allSG() is Dsimple by A1, A10;
  thus G.allSG() is Dsimple implies G is Dsimple by A3, A12;
  :: acyclic
  hereby
    assume A15: G is acyclic;
    now
      let H be _Graph;
      assume H in G.allSG();
      then H is Subgraph of G by Th1;
      hence H is acyclic by A15;
    end;
    hence G.allSG() is acyclic by GLIB_014:def 8;
  end;
  hereby
    assume A16: G.allSG() is acyclic;
    G | _GraphSelectors in G.allSG() by Th3;
    then A17: G | _GraphSelectors is acyclic by A16;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is acyclic by A17, GLIB_002:44;
  end;
  :: edgeless
  hereby
    assume A18: G is edgeless;
    now
      let H be _Graph;
      assume H in G.allSG();
      then H is Subgraph of G by Th1;
      hence H is edgeless by A18;
    end;
    hence G.allSG() is edgeless by GLIB_014:def 12;
  end;
  hereby
    assume A19: G.allSG() is edgeless;
    G | _GraphSelectors in G.allSG() by Th3;
    then A20: G | _GraphSelectors is edgeless by A19;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is edgeless by A20, GLIB_008:52;
  end;
end;

registration
  let G be loopless _Graph;
  cluster G.allSG() -> loopless;
  coherence by Th36;
end;

registration
  let G be non-multi _Graph;
  cluster G.allSG() -> non-multi;
  coherence by Th36;
end;

registration
  let G be non-Dmulti _Graph;
  cluster G.allSG() -> non-Dmulti;
  coherence by Th36;
end;

registration
  let G be simple _Graph;
  cluster G.allSG() -> simple;
  coherence;
end;

registration
  let G be Dsimple _Graph;
  cluster G.allSG() -> Dsimple;
  coherence;
end;

registration
  let G be acyclic _Graph;
  cluster G.allSG() -> acyclic;
  coherence by Th36;
end;

registration
  let G be edgeless _Graph;
  cluster G.allSG() -> edgeless;
  coherence by Th36;
end;

theorem Th37:
  the_Vertices_of G.allSG() = (bool the_Vertices_of G) \ {{}}
proof
  now
    let x be object;
    hereby
      assume x in the_Vertices_of G.allSG();
      then consider H being _Graph such that
        A1: H in G.allSG() & x = the_Vertices_of H by GLIB_014:def 14;
      H is Subgraph of G by A1, Th1;
      then the_Vertices_of H c= the_Vertices_of G by GLIB_000:def 32;
      then A2: x in bool the_Vertices_of G by A1;
      not x in {{}} by A1, TARSKI:def 1;
      hence x in (bool the_Vertices_of G) \ {{}} by A2, XBOOLE_0:def 5;
    end;
    reconsider X = x as set by TARSKI:1;
    assume x in (bool the_Vertices_of G) \ {{}};
    then x in bool the_Vertices_of G & not x in {{}} by XBOOLE_0:def 5;
    then reconsider X as non empty Subset of the_Vertices_of G by TARSKI:def 1;
    set S = the Function of {},X;
    set H = createGraph(X,{},S,S);
    the_Vertices_of H = X & H in G.allSG() by Lm1;
    hence x in the_Vertices_of G.allSG() by GLIB_014:def 14;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th38:
  the_Edges_of G.allSG() = bool the_Edges_of G
proof
  now
    let x be object;
    hereby
      assume x in the_Edges_of G.allSG();
      then consider H being _Graph such that
        A1: H in G.allSG() & x = the_Edges_of H by GLIB_014:def 15;
      H is Subgraph of G by A1, Th1;
      then the_Edges_of H c= the_Edges_of G by GLIB_000:def 32;
      hence x in bool the_Edges_of G by A1;
    end;
    reconsider X = x as set by TARSKI:1;
    set H = the plain inducedSubgraph of G, the_Vertices_of G, X;
    assume x in bool the_Edges_of G;
    then X c= the_Edges_of G;
    then A2: X c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
    the_Vertices_of G c= the_Vertices_of G;
    then A3: the_Edges_of H = X by A2, GLIB_000:def 37;
    H in G.allSG() by Th1;
    hence x in the_Edges_of G.allSG() by A3, GLIB_014:def 15;
  end;
  hence thesis by TARSKI:2;
end;

definition
  let G;
  func SubgraphRel(G) -> Relation of G.allSG() means
  :Def6:
  for H1, H2 being Element of G.allSG() holds [H1,H2] in it iff
    H1 is Subgraph of H2;
  existence
  proof
    defpred P[Element of G.allSG(), Element of G.allSG()]
      means $1 is Subgraph of $2;
    consider R being Relation of G.allSG() such that
      A1: for H1, H2 being Element of G.allSG() holds [H1,H2] in R
        iff P[H1,H2] from RELSET_1:sch 2;
    take R;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let R1, R2 be Relation of G.allSG();
    defpred P[Element of G.allSG(), Element of G.allSG()]
      means $1 is Subgraph of $2;
    assume that
      A2: for H1, H2 being Element of G.allSG() holds [H1,H2] in R1 iff
        P[H1,H2] and
      A3: for H1, H2 being Element of G.allSG() holds [H1,H2] in R2 iff
        P[H1,H2];
    thus thesis from RELSET_1:sch 4(A2,A3);
  end;
end;

theorem Th39:
  [H | _GraphSelectors, G | _GraphSelectors] in SubgraphRel(G)
proof
  A1: H | _GraphSelectors == H & G | _GraphSelectors == G by GLIB_000:128;
  A2: H | _GraphSelectors in G.allSG() &
    G | _GraphSelectors in G.allSG() by Th2, Th3;
  H | _GraphSelectors is Subgraph of G by A1, GLIB_000:92;
  then H| _GraphSelectors is Subgraph of G| _GraphSelectors by A1, GLIB_000:91;
  hence thesis by A2, Def6;
end;

theorem Th40:
  field SubgraphRel(G) = G.allSG()
proof
  field SubgraphRel(G) c= G.allSG() \/ G.allSG() by RELSET_1:8;
  then A1: field SubgraphRel(G) c= G.allSG();
  G.allSG() c= field SubgraphRel(G)
  proof
    let x be object;
    assume x in G.allSG();
    then reconsider H = x as plain Subgraph of G by Th1;
    H = H | _GraphSelectors by GLIB_000:128, GLIB_009:44;
    then [H, G | _GraphSelectors] in SubgraphRel(G) by Th39;
    hence x in field SubgraphRel(G) by RELAT_1:15;
  end;
  hence thesis by A1, XBOOLE_0:def 10;
end;

theorem Th41:
  SubgraphRel(G) partially_orders G.allSG()
proof
  now
    let x be object;
    assume x in G.allSG();
    then reconsider H = x as Element of G.allSG();
    H is Subgraph of H by GLIB_000:40;
    hence [x,x] in SubgraphRel(G) by Def6;
  end;
  then A1: SubgraphRel(G) is_reflexive_in G.allSG() by RELAT_2:def 1;
  now
    let x,y be object;
    assume that
      A2: x in G.allSG() & y in G.allSG() and
      A3: [x,y] in SubgraphRel(G) & [y,x] in SubgraphRel(G);
    reconsider H1 = x, H2 = y as Element of G.allSG() by A2;
    H1 is Subgraph of H2 & H2 is Subgraph of H1 by A3, Def6;
    hence x = y by GLIB_000:87, GLIB_009:44;
  end;
  then A4: SubgraphRel(G) is_antisymmetric_in G.allSG()
    by RELAT_2:def 4;
  now
    let x,y,z be object;
    assume that
      A5: x in G.allSG() & y in G.allSG() & z in G.allSG()
      and A6: [x,y] in SubgraphRel(G) & [y,z] in SubgraphRel(G);
    reconsider H1 = x, H2 = y, H3 = z as Element of G.allSG() by A5;
    H1 is Subgraph of H2 & H2 is Subgraph of H3 by A6, Def6;
    then H1 is Subgraph of H3 by GLIB_000:43;
    hence [x,z] in SubgraphRel(G) by Def6;
  end;
  hence thesis by A1, A4, RELAT_2:def 8, ORDERS_1:def 8;
end;

registration
  let G;
  cluster SubgraphRel(G) -> reflexive antisymmetric transitive
    being_partial-order;
  coherence
  proof
    A1: SubgraphRel(G) partially_orders G.allSG() by Th41;
    A2: G.allSG() = field SubgraphRel(G) by Th40;
    thus A3: SubgraphRel(G) is reflexive
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 9;
    thus A4: SubgraphRel(G) is antisymmetric
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 12;
    thus SubgraphRel(G) is transitive
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 16;
    hence thesis by A3, A4, ORDERS_1:def 5;
  end;
end;

theorem
  G | _GraphSelectors is_maximal_in SubgraphRel(G)
proof
  now
    G | _GraphSelectors in G.allSG() by Th3;
    hence A1: G | _GraphSelectors in field SubgraphRel(G) by Th40;
    given y being set such that
      A2: y in field SubgraphRel(G) & y <> G | _GraphSelectors and
      A3: [G | _GraphSelectors, y] in SubgraphRel(G);
    y in G.allSG() by A2, Th40;
    then reconsider H = y as plain Subgraph of G by Th1;
    H = H | _GraphSelectors by GLIB_000:128, GLIB_009:44;
    then [H, G | _GraphSelectors] in SubgraphRel(G) by Th39;
    hence contradiction by A1, A2, A3, RELAT_2:def 4, RELAT_2:def 12;
  end;
  hence thesis by ORDERS_1:def 12;
end;

theorem Th43:
  SubgraphRel(H) = (SubgraphRel G) |_2 H.allSG()
proof
  A1: H.allSG() c= G.allSG() by Th29;
  reconsider R = (SubgraphRel G) |_2 H.allSG()
    as Relation of H.allSG();
  now
    let H1, H2 be Element of H.allSG();
    hereby
      assume [H1,H2] in SubgraphRel(H);
      then A2: H1 is Subgraph of H2 by Def6;
      H1 in G.allSG() & H2 in G.allSG() by A1, TARSKI:def 3;
      then [H1,H2] in SubgraphRel(G) by A2, Def6;
      hence [H1,H2] in R by MMLQUER2:4;
    end;
    assume [H1,H2] in R;
    then A3: [H1,H2] in SubgraphRel(G) by MMLQUER2:4;
    then H1 in field SubgraphRel(G) & H2 in field SubgraphRel(G)
      by RELAT_1:15;
    then H1 in G.allSG() & H2 in G.allSG() by Th40;
    then H1 is Subgraph of H2 by A3, Def6;
    hence [H1,H2] in SubgraphRel(H) by Def6;
  end;
  hence thesis by RELSET_1:def 2;
end;

theorem Th44:
  for S being non empty Subset of G.allSG(), G9 being GraphUnion of S
  st (SubgraphRel G) |_2 S is being_linear-order holds
  for W being Walk of G9 ex H being Element of S st W is Walk of H
proof
  let S be non empty Subset of G.allSG(), G9 be GraphUnion of S;
  set R = (SubgraphRel G) |_2 S;
  assume A1: R is being_linear-order;
  defpred P[Walk of G9] means ex H being Element of S st $1 is Walk of H;
  A2: for W being trivial Walk of G9 holds P[W]
  proof
    let W be trivial Walk of G9;
    consider v9 being Vertex of G9 such that
      A3: W = G9.walkOf(v9) by GLIB_001:128;
    the_Vertices_of G9 = union the_Vertices_of S by GLIB_014:def 25;
    then consider V being set such that
      A4: v9 in V & V in the_Vertices_of S by TARSKI:def 4;
    consider H being _Graph such that
      A5: H in S & V = the_Vertices_of H by A4, GLIB_014:def 14;
    reconsider H as Element of S by A5;
    take H;
    reconsider v = v9 as Vertex of H by A4, A5;
    W = <* v *> by A3, GLIB_001:def 4
      .= H.walkOf(v) by GLIB_001:def 4;
    hence thesis;
  end;
  A6: for W being Walk of G9, e being object
    st e in W.last().edgesInOut() & P[W] holds P[W.addEdge(e)]
  proof
    let W be Walk of G9, e be object;
    assume A7: e in W.last().edgesInOut() & P[W];
    then e in the_Edges_of G9;
    then e in union the_Edges_of S by GLIB_014:def 25;
    then consider E being set such that
      A8: e in E & E in the_Edges_of S by TARSKI:def 4;
    consider H2 being _Graph such that
      A9: H2 in S & E = the_Edges_of H2 by A8, GLIB_014:def 15;
    reconsider H2 as Element of S by A9;
    consider H1 being Element of S such that
      A10: W is Walk of H1 by A7;
    R is reflexive connected by A1, ORDERS_1:def 6;
    then A11: R is_strongly_connected_in field R by RELAT_2:def 15;
    A12: field SubgraphRel(G) = G.allSG() by Th40;
    then field R = S by ORDERS_1:71;
    then A13: H1 in field R & H2 in field R;
    then A14: H1 in G.allSG() & H2 in G.allSG()
      by A12, WELLORD1:12;
    consider w being Vertex of G9 such that
      A15: e Joins W.last(),w,G9 by A7, GLIB_000:64;
    A16: H1 is Subgraph of G9 & H2 is Subgraph of G9 by GLIB_014:21;
    then A17: e Joins W.last(),w,H2 by A8, A9, A15, GLIB_000:73;
    per cases by A11, A13, RELAT_2:def 7;
    suppose [H1,H2] in R;
      then [H1,H2] in SubgraphRel(G) by MMLQUER2:4;
      then H1 is Subgraph of H2 by A14, Def6;
      then reconsider W2 = W as Walk of H2 by A10, GLIB_001:167;
      take H2;
      W.last() = W2.last() by GLIB_001:16;
      then e in W2.last().edgesInOut() by A17, GLIB_000:62;
      then W.addEdge(e) = W2.addEdge(e) by A16, GLIB_001:174;
      hence thesis;
    end;
    suppose [H2,H1] in R;
      then [H2,H1] in SubgraphRel(G) by MMLQUER2:4;
      then H2 is Subgraph of H1 by A14, Def6;
      then A18: e Joins W.last(),w,H1 by A17, GLIB_000:72;
      reconsider W1 = W as Walk of H1 by A10;
      take H1;
      W.last() = W1.last() by GLIB_001:16;
      then e in W1.last().edgesInOut() by A18, GLIB_000:62;
      then W.addEdge(e) = W1.addEdge(e) by A16, GLIB_001:174;
      hence thesis;
    end;
  end;
  for W being Walk of G9 holds P[W] from GLIB_009:sch 1(A2,A6);
  hence thesis;
end;

begin :: Induced Subgraph set

definition
  let G;
  func G.allInducedSG() -> Subset of G.allSG() equals
  the set of all the plain inducedSubgraph of G,V
    where V is non empty Subset of the_Vertices_of G;
  coherence
  proof
    set S = the set of all the plain inducedSubgraph of G,V
      where V is non empty Subset of the_Vertices_of G;
    now
      let x be object;
      assume x in S;
      then consider V being non empty Subset of the_Vertices_of G such that
        A1: x = the plain inducedSubgraph of G,V;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th45:
  G2 in G1.allInducedSG() iff
    ex V being non empty Subset of the_Vertices_of G1
    st G2 is plain inducedSubgraph of G1,V
proof
  hereby
    assume G2 in G1.allInducedSG();
    then consider V being non empty Subset of the_Vertices_of G1 such that
      A1: G2 = the plain inducedSubgraph of G1,V;
    take V;
    thus G2 is plain inducedSubgraph of G1,V by A1;
  end;
  given V being non empty Subset of the_Vertices_of G1 such that
    A2: G2 is plain inducedSubgraph of G1,V;
  set H = the plain inducedSubgraph of G1,V;
  G2 = H by A2, GLIB_000:93, GLIB_009:44;
  hence G2 in G1.allInducedSG();
end;

registration
  let G be vertex-finite _Graph;
  cluster G.allInducedSG() -> finite;
  coherence
  proof
    set V = the_Vertices_of G;
    deffunc I(object) = the plain inducedSubgraph of G,Segm $1;
    consider f being Function such that
      A1: dom f = bool V and
      A2: for x being object st x in bool V holds f.x = I(x)
      from FUNCT_1:sch 3;
    A3: rng f is finite by A1, FINSET_1:8;
    now
      let h be object;
      assume A4: h in G.allInducedSG();
      then reconsider H = h as _Graph;
      consider W being non empty Subset of the_Vertices_of G such that
        A5: H is plain inducedSubgraph of G,W by A4, Th45;
      A6: Segm W = W by ORDINAL1:def 17;
      f.W = the plain inducedSubgraph of G,W by A2, A6;
      then H = f.W by A5, GLIB_000:93, GLIB_009:44;
      hence h in rng f by A1, FUNCT_1:def 3;
    end;
    then G.allInducedSG() c= rng f by TARSKI:def 3;
    hence thesis by A3;
  end;
end;

theorem Th46:
  for V being non empty Subset of the_Vertices_of G
  for H being inducedSubgraph of G, V
  holds H | _GraphSelectors in G.allInducedSG()
proof
  let V be non empty Subset of the_Vertices_of G;
  let H be inducedSubgraph of G, V;
  H | _GraphSelectors is inducedSubgraph of G, V by GLIB_000:128, GLIB_000:101;
  hence thesis by Th45;
end;

theorem Th47:
  G | _GraphSelectors in G.allInducedSG()
proof
  the_Vertices_of G c= the_Vertices_of G;
  then A1: the_Vertices_of G is non empty Subset of the_Vertices_of G;
  G is inducedSubgraph of G, the_Vertices_of G by GLIB_000:100;
  hence thesis by A1, Th46;
end;

registration
  let G;
  cluster G.allInducedSG() -> non empty \/-tolerating plain;
  coherence by Th47;
end;

theorem Th48:
  G2.allInducedSG() c= G1.allInducedSG() iff
    ex V being non empty Subset of the_Vertices_of G1
    st G2 is inducedSubgraph of G1,V
proof
  hereby
    assume A1: G2.allInducedSG() c= G1.allInducedSG();
    G2 | _GraphSelectors in G2.allInducedSG() by Th47;
    then consider V being non empty Subset of the_Vertices_of G1 such that
      A2: G2 | _GraphSelectors is plain inducedSubgraph of G1,V by A1, Th45;
    take V;
    G2 == G2 | _GraphSelectors by GLIB_000:128;
    hence G2 is inducedSubgraph of G1, V by A2, GLIB_000:101;
  end;
  given V being non empty Subset of the_Vertices_of G1 such that
    A3: G2 is inducedSubgraph of G1,V;
  now
    let x be object;
    assume x in G2.allInducedSG();
    then consider V2 being non empty Subset of the_Vertices_of G2 such that
      A4: x is plain inducedSubgraph of G2,V2 by Th45;
    the_Vertices_of G2 = V by A3, GLIB_000:def 37;
    then A5: V2 c= V;
    then A6: V2 is non empty Subset of the_Vertices_of G1 by XBOOLE_1:1;
    then x is inducedSubgraph of G1,V2 by A3, A4, A5, CHORD:29;
    hence x in G1.allInducedSG() by A4, A6, Th45;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th49:
  G1 == G2 iff G1.allInducedSG() = G2.allInducedSG()
proof
  set V1 = the_Vertices_of G1, V2 = the_Vertices_of G2;
  hereby
    assume A1: G1 == G2;
    G1 is inducedSubgraph of G1, V1 & G2 is inducedSubgraph of G2, V2
      by GLIB_000:100;
    then A2: G1 is inducedSubgraph of G2, V2 & G2 is inducedSubgraph of G1, V1
      by A1, GLIB_000:101;
    V1 c= V1 & V2 c= V2;
    then G1.allInducedSG() c= G2.allInducedSG() &
      G2.allInducedSG() c= G1.allInducedSG() by A2, Th48;
    hence G1.allInducedSG() = G2.allInducedSG()
      by XBOOLE_0:def 10;
  end;
  assume A3: G1.allInducedSG() = G2.allInducedSG();
  then consider V2 being non empty Subset of the_Vertices_of G2 such that
    A4: G1 is inducedSubgraph of G2, V2 by Th48;
  consider V1 being non empty Subset of the_Vertices_of G1 such that
    A5: G2 is inducedSubgraph of G1, V1 by A3, Th48;
  thus thesis by A4, A5, GLIB_000:87;
end;

theorem Th50:
  for F being PGraphMapping of G1, G2 st F is total onto
  holds G2.allInducedSG() c= rng(SG2SGFunc(F) | G1.allInducedSG())
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is total onto;
  set f = SG2SGFunc(F) | G1.allInducedSG();
  A2: dom f = G1.allInducedSG() by FUNCT_2:def 1;
  now
    let x be object;
    assume A3: x in G2.allInducedSG();
    A4: rng F == G2 by A1, GLIB_010:56;
    then x in (rng F).allInducedSG() by A3, Th49;
    then consider V2 being non empty Subset of the_Vertices_of rng F
      such that A5: x = the plain inducedSubgraph of rng F,V2;
    reconsider H2 = x as plain inducedSubgraph of rng F,V2 by A5;
    set H1 = the plain inducedSubgraph of G1, F_V"the_Vertices_of H2;
    reconsider y = H1 as object;
    rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12
      .= the_Vertices_of rng F by A4, GLIB_000:def 34;
    then A6: F_V"V2 <> {} by RELAT_1:139;
    the_Vertices_of H2 = V2 by GLIB_000:def 37;
    then A7: H1 in G1.allInducedSG() by A6;
    then A8: y in dom f by A2;
    A9: (SG2SGFunc F).H1 = rng(F | H1) by Def5;
    dom F_E = the_Edges_of G1 by A1, GLIB_010:def 11;
    then G1.edgesBetween(F_V"the_Vertices_of H2) c= dom F_E;
    then (SG2SGFunc F).H1 = H2 by A1, A9, GLIB_009:44, GLIBPRE1:101;
    then x = f.y by A7, FUNCT_1:49;
    hence x in rng f by A8, FUNCT_1:def 3;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th51:
  for F being PGraphMapping of G1, G2 st F is total continuous
  holds rng(SG2SGFunc(F) | G1.allInducedSG()) c= G2.allInducedSG()
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is total continuous;
  set f = SG2SGFunc(F) | G1.allInducedSG();
  A2: dom f = G1.allInducedSG() by FUNCT_2:def 1;
  now
    let x be object;
    assume x in rng f;
    then consider y being object such that
      A3: y in dom f & x = f.y by FUNCT_1:def 3;
    consider V1 being non empty Subset of the_Vertices_of G1 such that
      A4: y = the plain inducedSubgraph of G1, V1 by A2, A3;
    reconsider H1 = y as inducedSubgraph of G1, V1 by A4;
    dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
    then A5: F_V.:V1 is non empty Subset of the_Vertices_of G2 by RELAT_1:119;
    G1 == dom F by A1, GLIB_010:55;
    then A6: the_Vertices_of G1 = the_Vertices_of dom F by GLIB_000:def 34;
    x = SG2SGFunc(F).y by A3, FUNCT_1:47
      .= rng(F | H1) by A4, Def5;
    then x is plain inducedSubgraph of G2, F_V.:V1 by A1, A6, GLIBPRE1:102;
    hence x in G2.allInducedSG() by A5, Th45;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th52:
  for F being PGraphMapping of G1, G2 st F is isomorphism
  holds rng(SG2SGFunc(F) | G1.allInducedSG())  = G2.allInducedSG()
proof
  let F be PGraphMapping of G1, G2;
  assume F is isomorphism;
  then rng(SG2SGFunc(F) | G1.allInducedSG())
    c= G2.allInducedSG() & G2.allInducedSG()
    c= rng(SG2SGFunc(F) | G1.allInducedSG())
    by Th50, Th51;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  G2 is G1-Disomorphic implies
    G1.allInducedSG(),G2.allInducedSG() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allInducedSG();
  A2: dom f = G1.allInducedSG() by FUNCT_2:def 1;
  A3: rng f = G2.allInducedSG() by A1, Th52;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allInducedSG();
    then consider V being non empty Subset of the_Vertices_of G1 such that
      A6: G is plain inducedSubgraph of G1, V by Th45;
    reconsider H = G as plain inducedSubgraph of G1, V by A6;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A7: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph by A7, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem
  G2 is G1-isomorphic implies
    G1.allInducedSG(),G2.allInducedSG() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allInducedSG();
  A2: dom f = G1.allInducedSG() by FUNCT_2:def 1;
  A3: rng f = G2.allInducedSG() by A1, Th52;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allInducedSG();
    then consider V being non empty Subset of the_Vertices_of G1 such that
      A6: G is plain inducedSubgraph of G1, V by Th45;
    reconsider H = G as plain inducedSubgraph of G1, V by A6;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A7: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A7, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem Th55:
  G is GraphUnion of G.allInducedSG()
proof
  set G9 = the GraphUnion of G.allInducedSG();
  set G8 = the GraphUnion of {G};
  G | _GraphSelectors in G.allInducedSG() by Th47;
  then A1: G | _GraphSelectors is Subgraph of G9 by GLIB_014:21;
  G == G | _GraphSelectors by GLIB_000:128;
  then A2: G is Subgraph of G9 by A1, GLIB_000:92;
  now
    let H2 be Element of G.allInducedSG();
    reconsider H1 = G as Element of {G} by TARSKI:def 1;
    take H1;
    thus H2 is Subgraph of H1;
  end;
  then G9 is Subgraph of G8 by GLIBPRE1:118;
  then G9 is Subgraph of G by GLIB_000:91, GLIB_014:24;
  hence thesis by A2, GLIB_000:87, GLIB_014:22;
end;

theorem Th56:
  (G is loopless iff G.allInducedSG() is loopless) &
  (G is non-multi iff G.allInducedSG() is non-multi) &
  (G is non-Dmulti iff G.allInducedSG() is non-Dmulti) &
  (G is simple iff G.allInducedSG() is simple) &
  (G is Dsimple iff G.allInducedSG() is Dsimple) &
  (G is acyclic iff G.allInducedSG() is acyclic) &
  (G is edgeless iff G.allInducedSG() is edgeless) &
  (G is chordal iff G.allInducedSG() is chordal) &
  (G is loopfull iff G.allInducedSG() is loopfull)
proof
  :: loopless
  thus A1: G is loopless implies G.allInducedSG() is loopless
  proof
    assume A2: G is loopless;
    G is GraphUnion of G.allInducedSG() by Th55;
    hence G.allInducedSG() is loopless by A2, GLIB_014:23;
  end;
  thus A3: G.allInducedSG() is loopless implies G is loopless
  proof
    assume A4: G.allInducedSG() is loopless;
    G is GraphUnion of G.allInducedSG() by Th55;
    hence G is loopless by A4;
  end;
  :: non-multi
  thus A5: G is non-multi implies G.allInducedSG() is non-multi
  proof
    assume G is non-multi;
    then G.allSG() is non-multi;
    hence thesis;
  end;
  thus A6: G.allInducedSG() is non-multi implies G is non-multi
  proof
    assume A7: G.allInducedSG() is non-multi;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A8: G | _GraphSelectors is non-multi by A7;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A8, GLIB_000:89;
  end;
  :: non-Dmulti
  thus A9: G is non-Dmulti implies G.allInducedSG() is non-Dmulti
  proof
    assume G is non-Dmulti;
    then G.allSG() is non-Dmulti;
    hence thesis;
  end;
  thus A10: G.allInducedSG() is non-Dmulti implies G is non-Dmulti
  proof
    assume A11: G.allInducedSG() is non-Dmulti;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A12: G | _GraphSelectors is non-Dmulti by A11;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A12, GLIB_000:89;
  end;
  :: simple
  thus G is simple implies G.allInducedSG() is simple by A1, A5;
  thus G.allInducedSG() is simple implies G is simple by A3, A6;
  :: Dsimple
  thus G is Dsimple implies G.allInducedSG() is Dsimple by A1, A9;
  thus G.allInducedSG() is Dsimple implies G is Dsimple by A3, A10;
  :: acyclic
  hereby
    assume G is acyclic;
    then G.allSG() is acyclic;
    hence G.allInducedSG() is acyclic;
  end;
  hereby
    assume A13: G.allInducedSG() is acyclic;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A14: G | _GraphSelectors is acyclic by A13;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is acyclic by A14, GLIB_002:44;
  end;
  :: edgeless
  hereby
    assume G is edgeless;
    then G.allSG() is edgeless;
    hence G.allInducedSG() is edgeless;
  end;
  hereby
    assume A15: G.allInducedSG() is edgeless;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A16: G | _GraphSelectors is edgeless by A15;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is edgeless by A16, GLIB_008:52;
  end;
  :: chordal
  hereby
    assume A17: G is chordal;
    now
      let H be _Graph;
      assume H in G.allInducedSG();
      then consider V being non empty Subset of the_Vertices_of G such that
        A18: H is plain inducedSubgraph of G,V by Th45;
      thus H is chordal by A17, A18;
    end;
    hence G.allInducedSG() is chordal by GLIB_014:def 11;
  end;
  hereby
    assume A19: G.allInducedSG() is chordal;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A20: G | _GraphSelectors is chordal by A19;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is chordal by A20, CHORD:95;
  end;
  :: loopfull
  hereby
    assume A21: G is loopfull;
    now
      let H be _Graph;
      assume H in G.allInducedSG();
      then consider V being non empty Subset of the_Vertices_of G such that
        A22: H is plain inducedSubgraph of G,V by Th45;
      thus H is loopfull by A21, A22;
    end;
    hence G.allInducedSG() is loopfull by GLIB_014:def 13;
  end;
  hereby
    assume A23: G.allInducedSG() is loopfull;
    G | _GraphSelectors in G.allInducedSG() by Th47;
    then A24: G | _GraphSelectors is loopfull by A23;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is loopfull by A24, GLIB_012:4;
  end;
end;

registration
  let G be loopless _Graph;
  cluster G.allInducedSG() -> loopless;
  coherence;
end;

registration
  let G be non-multi _Graph;
  cluster G.allInducedSG() -> non-multi;
  coherence;
end;

registration
  let G be non-Dmulti _Graph;
  cluster G.allInducedSG() -> non-Dmulti;
  coherence;
end;

registration
  let G be simple _Graph;
  cluster G.allInducedSG() -> simple;
  coherence;
end;

registration
  let G be Dsimple _Graph;
  cluster G.allInducedSG() -> Dsimple;
  coherence;
end;

registration
  let G be acyclic _Graph;
  cluster G.allInducedSG() -> acyclic;
  coherence;
end;

registration
  let G be edgeless _Graph;
  cluster G.allInducedSG() -> edgeless;
  coherence;
end;

registration
  let G be chordal _Graph;
  cluster G.allInducedSG() -> chordal;
  coherence by Th56;
end;

registration
  let G be loopfull _Graph;
  cluster G.allInducedSG() -> loopfull;
  coherence by Th56;
end;

theorem Th57:
  G is edgeless iff G.allInducedSG() = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G
proof
  set S = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G;
  hereby
    assume A1: G is edgeless;
    G.allInducedSG() c= G.allSG();
    then A2: G.allInducedSG() c= S by A1, Th9;
    now
      let x be object;
      assume x in S;
      then consider V being non empty Subset of the_Vertices_of G such that
        A3: x = createGraph(V);
      set H = createGraph(V);
      A4: G.edgesBetween(V) = the_Edges_of H by A1;
      A5: the_Vertices_of H = V;
      H is inducedSubgraph of G,V by A4, A5, GLIB_000:def 37;
      hence x in G.allInducedSG() by A3, Th45;
    end;
    then S c= G.allInducedSG() by TARSKI:def 3;
    hence G.allInducedSG() = S by A2, XBOOLE_0:def 10;
  end;
  assume A6: G.allInducedSG() = S;
  G | _GraphSelectors in G.allInducedSG() by Th47;
  then consider V being non empty Subset of the_Vertices_of G such that
    A7: G | _GraphSelectors = createGraph(V) by A6;
  A8: G == G | _GraphSelectors by GLIB_000:128;
  the_Edges_of (G | _GraphSelectors) = {} by A7;
  then the_Edges_of G = {} by A8, GLIB_000:def 34;
  hence G is edgeless;
end;

theorem
  G is edgeless iff G.allSG() = G.allInducedSG()
proof
 set S = the set of all createGraph(V)
   where V is non empty Subset of the_Vertices_of G;
  hereby
    assume A1: G is edgeless;
    hence G.allSG() = S by Th9
      .= G.allInducedSG() by A1, Th57;
  end;
  assume A2: G.allSG() = G.allInducedSG();
  set H = createGraph([#]the_Vertices_of G);
  consider V being non empty Subset of the_Vertices_of G such that
    A3: H is plain inducedSubgraph of G,V by A2, Lm1, Th45;
  A4: V = the_Vertices_of H by A3, GLIB_000:def 37
    .= the_Vertices_of G;
  {} = the_Edges_of H
    .= G.edgesBetween(V) by A3, GLIB_000:def 37
    .= the_Edges_of G by A4, GLIB_000:34;
  hence thesis;
end;

theorem
  the_Vertices_of G.allInducedSG() = (bool the_Vertices_of G) \ {{}}
proof
  the_Vertices_of G.allInducedSG() c= the_Vertices_of G.allSG()
    by GLIBPRE1:115;
  then A1: the_Vertices_of G.allInducedSG() c= (bool the_Vertices_of G) \ {{}}
    by Th37;
  now
    let x be object;
    reconsider X = x as set by TARSKI:1;
    assume x in (bool the_Vertices_of G) \ {{}};
    then x in bool the_Vertices_of G & not x in {{}} by XBOOLE_0:def 5;
    then reconsider X as non empty Subset of the_Vertices_of G by TARSKI:def 1;
    set H = the plain inducedSubgraph of G,X;
    the_Vertices_of H = X & H in G.allInducedSG() by GLIB_000:def 37;
    hence x in the_Vertices_of G.allInducedSG() by GLIB_014:def 14;
  end;
  then (bool the_Vertices_of G)\{{}} c= the_Vertices_of G.allInducedSG()
    by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

begin :: Spanning Subgraph set

::$INSERT The following functor could also be named G.allFactors().
definition
  let G;
  func G.allSpanningSG() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is spanning };
  coherence
  proof
    now
      let x be object;
      assume x in { H
        where H is Element of [#]G.allSG() : H is spanning };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is spanning;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th60:
  G2 in G1.allSpanningSG() iff G2 is plain spanning Subgraph of G1
proof
  hereby
    assume G2 in G1.allSpanningSG();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is spanning;
    thus G2 is plain spanning Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain spanning Subgraph of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th61:
  for H being spanning Subgraph of G
  holds H | _GraphSelectors in G.allSpanningSG()
proof
  let H be spanning Subgraph of G;
  H | _GraphSelectors == H by GLIB_000:128;
  then H | _GraphSelectors is spanning Subgraph of G by GLIB_000:171;
  hence thesis by Th60;
end;

theorem Th62:
  G | _GraphSelectors in G.allSpanningSG()
proof
  reconsider H = G as Subgraph of G by GLIB_000:40;
  the_Vertices_of H = the_Vertices_of G;
  then H is spanning by GLIB_000:def 33;
  hence thesis by Th61;
end;

theorem Th63:
  createGraph([#]the_Vertices_of G) in G.allSpanningSG()
proof
  set H = createGraph([#]the_Vertices_of G);
  reconsider H as Subgraph of G;
  the_Vertices_of H = the_Vertices_of G;
  then H is spanning by GLIB_000:def 33;
  hence thesis by Th60;
end;

theorem Th64:
  for G being non edgeless _Graph, e being Edge of G
  for H being plain addVertices of createGraph(e), the_Vertices_of G
  holds H in G.allSpanningSG()
proof
  let G be non edgeless _Graph, e be Edge of G;
  let H be plain addVertices of createGraph(e), the_Vertices_of G;
  A1: the_Vertices_of H
     = the_Vertices_of createGraph(e) \/ the_Vertices_of G by GLIB_006:def 10
    .= the_Vertices_of G by XBOOLE_1:12;
  the_Vertices_of G c= the_Vertices_of G;
  then H is spanning Subgraph of G by A1, Th21, GLIB_000:def 33;
  hence thesis by Th60;
end;

registration
  let G be _Graph;
  cluster G.allSpanningSG() -> non empty \/-tolerating plain;
  coherence by Th62;
end;

theorem Th65:
  G2.allSpanningSG() c= G1.allSpanningSG() iff G2 is spanning Subgraph of G1
proof
  hereby
    assume A1: G2.allSpanningSG() c= G1.allSpanningSG();
    G2 | _GraphSelectors in G2.allSpanningSG() by Th62;
    then G2 | _GraphSelectors is spanning Subgraph of G1 by A1, Th60;
    hence G2 is spanning Subgraph of G1 by GLIB_000:171, GLIB_000:128;
  end;
  assume A2: G2 is spanning Subgraph of G1;
  now
    let x be object;
    assume x in G2.allSpanningSG();
    then reconsider H = x as plain spanning Subgraph of G2 by Th60;
    the_Vertices_of H = the_Vertices_of G2 by GLIB_000:def 33
      .= the_Vertices_of G1 by A2, GLIB_000:def 33;
    then H is plain spanning Subgraph of G1
      by A2, GLIB_000:43, GLIB_000:def 33;
    hence x in G1.allSpanningSG() by Th60;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  G1 == G2 iff G1.allSpanningSG() = G2.allSpanningSG()
proof
  hereby
    assume A1: G1 == G2;
    then the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34;
    then G1 is spanning Subgraph of G2 & G2 is spanning Subgraph of G1
      by A1, GLIB_000:87, GLIB_000:def 33;
    then G1.allSpanningSG() c= G2.allSpanningSG() &
      G2.allSpanningSG() c= G1.allSpanningSG() by Th65;
    hence G1.allSpanningSG() = G2.allSpanningSG()
      by XBOOLE_0:def 10;
  end;
  assume G1.allSpanningSG() = G2.allSpanningSG();
  then G1 is spanning Subgraph of G2 & G2 is spanning Subgraph of G1
    by Th65;
  hence thesis by GLIB_000:87;
end;

theorem Th67:
  for F being PGraphMapping of G1, G2 st rng F_V = the_Vertices_of G2
  holds rng(SG2SGFunc(F) | G1.allSpanningSG()) c= G2.allSpanningSG()
proof
  let F be PGraphMapping of G1, G2;
  assume A1: rng F_V = the_Vertices_of G2;
  set f = SG2SGFunc(F) | G1.allSpanningSG();
  A3: dom f = G1.allSpanningSG() by FUNCT_2:def 1;
  now
    let y be object;
    assume A4: y in rng f;
    then consider x being object such that
      A5: x in dom f & f.x = y by FUNCT_1:def 3;
    consider H1 being Element of [#]G1.allSG() such that
      A6: x = H1 & H1 is spanning by A3, A5;
    reconsider H2 = y as Element of [#]G2.allSG() by A4;
    A7: (F|H1)_V = F_V | the_Vertices_of G1 by A6, GLIB_000:def 33
      .= F_V;
    H2 = SG2SGFunc(F).x by A5,FUNCT_1:47
      .= rng(F|H1) by A6, Def5;
    then H2 is spanning by A1, A7;
    hence y in G2.allSpanningSG();
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th68:
  for F being PGraphMapping of G1, G2 st F is onto & F_V is one-to-one total
  holds rng(SG2SGFunc(F) | G1.allSpanningSG()) = G2.allSpanningSG()
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F) | G1.allSpanningSG();
  assume A1: F is onto & F_V is one-to-one total;
  then rng F_V = the_Vertices_of G2 by GLIB_010:def 12;
  then A2: rng f c= G2.allSpanningSG() by Th67;
  now
    let y be object;
    assume y in G2.allSpanningSG();
    then consider H2 being Element of [#]G2.allSG() such that
      A3: y = H2 & H2 is spanning;
    H2 in G2.allSG();
    then H2 in rng SG2SGFunc(F) by A1, Th32;
    then consider x being object such that
      A4: x in dom SG2SGFunc(F) & (SG2SGFunc F).x = H2
      by FUNCT_1:def 3;
    reconsider H1 = x as plain Subgraph of G1 by A4, Th1;
    dom F_V = the_Vertices_of G1 by A1, PARTFUN1:def 2;
    then A5: the_Vertices_of H1 c= dom F_V;
    then dom((F|H1)_V) <> {} by RELAT_1:62;
    then A6: F|H1 is non empty;
    A7: H2 = rng(F|H1) by A4, Def5;
    the_Vertices_of H1 = F_V"(F_V.:the_Vertices_of H1) by A1, A5, FUNCT_1:94
      .= F_V"rng(F_V|the_Vertices_of H1) by RELAT_1:115
      .= F_V"the_Vertices_of rng(F|H1) by A6, GLIB_010:54
      .= F_V"the_Vertices_of G2 by A3, A7, GLIB_000:def 33
      .= dom F_V by RELSET_1:22
      .= the_Vertices_of G1 by A1, PARTFUN1:def 2;
    then H1 is spanning by GLIB_000:def 33;
    then A8: x in dom f by A4, Th60, RELAT_1:57;
    then H2 = f.x by A4, FUNCT_1:47;
    hence y in rng f by A3, A8, FUNCT_1:3;
  end;
  then G2.allSpanningSG() c= rng f by TARSKI:def 3;
  hence thesis by A2, XBOOLE_0:def 10;
end;

theorem Th69:
  for F being PGraphMapping of G1, G2 st F is isomorphism
  holds rng(SG2SGFunc(F) | G1.allSpanningSG()) = G2.allSpanningSG()
proof
  let F be PGraphMapping of G1, G2;
  assume F is isomorphism;
  then F is onto & F_V is one-to-one & dom F_V = the_Vertices_of G1
    by GLIB_010:def 11;
  then F is onto & F_V is one-to-one & F_V is total by PARTFUN1:def 2;
  hence thesis by Th68;
end;

theorem
  G2 is G1-Disomorphic implies
    G1.allSpanningSG(),G2.allSpanningSG() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allSpanningSG();
  A2: dom f = G1.allSpanningSG() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningSG() by A1, Th69;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningSG();
    then reconsider H = G as plain spanning Subgraph of G1 by Th60;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem
  G2 is G1-isomorphic implies
    G1.allSpanningSG(),G2.allSpanningSG() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allSpanningSG();
  A2: dom f = G1.allSpanningSG() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningSG() by A1, Th69;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningSG();
    then reconsider H = G as plain spanning Subgraph of G1 by Th60;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem Th72:
  G is GraphUnion of G.allSpanningSG()
proof
  set G9 = the GraphUnion of G.allSpanningSG();
  set G8 = the GraphUnion of {G};
  G | _GraphSelectors in G.allSpanningSG() by Th62;
  then A1: G | _GraphSelectors is Subgraph of G9 by GLIB_014:21;
  G == G | _GraphSelectors by GLIB_000:128;
  then A2: G is Subgraph of G9 by A1, GLIB_000:92;
  now
    let H2 be Element of G.allSpanningSG();
    reconsider H1 = G as Element of {G} by TARSKI:def 1;
    take H1;
    thus H2 is Subgraph of H1;
  end;
  then G9 is Subgraph of G8 by GLIBPRE1:118;
  then G9 is Subgraph of G by GLIB_000:91, GLIB_014:24;
  hence thesis by A2, GLIB_000:87, GLIB_014:22;
end;

theorem
  (G is loopless iff G.allSpanningSG() is loopless) &
  (G is non-multi iff G.allSpanningSG() is non-multi) &
  (G is non-Dmulti iff G.allSpanningSG() is non-Dmulti) &
  (G is simple iff G.allSpanningSG() is simple) &
  (G is Dsimple iff G.allSpanningSG() is Dsimple) &
  (G is acyclic iff G.allSpanningSG() is acyclic) &
  (G is edgeless iff G.allSpanningSG() is edgeless)
proof
  :: loopless
  thus G is loopless implies G.allSpanningSG() is loopless;
  thus A1: G.allSpanningSG() is loopless implies G is loopless
  proof
    assume A2: G.allSpanningSG() is loopless;
    G is GraphUnion of G.allSpanningSG() by Th72;
    hence G is loopless by A2;
  end;
  :: non-multi
  thus G is non-multi implies G.allSpanningSG() is non-multi;
  thus A3: G.allSpanningSG() is non-multi implies G is non-multi
  proof
    assume A4: G.allSpanningSG() is non-multi;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    then A5: G | _GraphSelectors is non-multi by A4;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A5, GLIB_000:89;
  end;
  :: non-Dmulti
  thus G is non-Dmulti implies G.allSpanningSG() is non-Dmulti;
  thus A6: G.allSpanningSG() is non-Dmulti implies G is non-Dmulti
  proof
    assume A7: G.allSpanningSG() is non-Dmulti;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    then A8: G | _GraphSelectors is non-Dmulti by A7;
    G == G | _GraphSelectors by GLIB_000:128;
    hence thesis by A8, GLIB_000:89;
  end;
  :: simple
  thus G is simple implies G.allSpanningSG() is simple;
  thus G.allSpanningSG() is simple implies G is simple by A1, A3;
  :: Dsimple
  thus G is Dsimple implies G.allSpanningSG() is Dsimple;
  thus G.allSpanningSG() is Dsimple implies G is Dsimple by A1, A6;
  :: acyclic
  thus G is acyclic implies G.allSpanningSG() is acyclic;
  hereby
    assume A9: G.allSpanningSG() is acyclic;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    then A10: G | _GraphSelectors is acyclic by A9;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is acyclic by A10, GLIB_002:44;
  end;
  :: edgeless
  thus G is edgeless implies G.allSpanningSG() is edgeless;
  hereby
    assume A11: G.allSpanningSG() is edgeless;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    then A12: G | _GraphSelectors is edgeless by A11;
    G == G | _GraphSelectors by GLIB_000:128;
    hence G is edgeless by A12, GLIB_008:52;
  end;
end;

registration
  let G be loopless _Graph;
  cluster G.allSpanningSG() -> loopless;
  coherence;
end;

registration
  let G be non-multi _Graph;
  cluster G.allSpanningSG() -> non-multi;
  coherence;
end;

registration
  let G be non-Dmulti _Graph;
  cluster G.allSpanningSG() -> non-Dmulti;
  coherence;
end;

registration
  let G be simple _Graph;
  cluster G.allSpanningSG() -> simple;
  coherence;
end;

registration
  let G be Dsimple _Graph;
  cluster G.allSpanningSG() -> Dsimple;
  coherence;
end;

registration
  let G be acyclic _Graph;
  cluster G.allSpanningSG() -> acyclic;
  coherence;
end;

registration
  let G be edgeless _Graph;
  cluster G.allSpanningSG() -> edgeless;
  coherence;
end;

theorem
  G is edgeless iff G.allSpanningSG() = {G | _GraphSelectors}
proof
  hereby
    assume A1: G is edgeless;
    now
      let x be object;
      hereby
        assume x in G.allSpanningSG();
        then reconsider H = x as plain spanning Subgraph of G by Th60;
        the_Edges_of H = {} by A1;
        then the_Edges_of H = the_Edges_of G by A1;
        then G == H & G == G | _GraphSelectors by GLIB_000:128, GLIB_000:118;
        hence x = G | _GraphSelectors by GLIB_000:85, GLIB_009:44;
      end;
      assume x = G | _GraphSelectors;
      hence x in G.allSpanningSG() by Th62;
    end;
    hence G.allSpanningSG() = {G | _GraphSelectors} by TARSKI:def 1;
  end;
  assume A2: G.allSpanningSG() = {G | _GraphSelectors};
  set H = the plain removeEdges of G, the_Edges_of G;
  H in G.allSpanningSG() by Th60;
  then A3: H = G | _GraphSelectors by A2, TARSKI:def 1;
  G == G | _GraphSelectors by GLIB_000:128;
  then the_Edges_of G = the_Edges_of H by A3, GLIB_000:def 34
    .= {};
  hence thesis;
end;

theorem Th75:
  the_Vertices_of G.allSpanningSG() = { the_Vertices_of G }
proof
  now
    let x be object;
    hereby
      assume x in the_Vertices_of G.allSpanningSG();
      then consider H being _Graph such that
        A1: H in G.allSpanningSG() & x = the_Vertices_of H
        by GLIB_014:def 14;
      H is spanning Subgraph of G by A1, Th60;
      hence x = the_Vertices_of G by A1, GLIB_000:def 33;
    end;
    assume A2: x = the_Vertices_of G;
    set H = the plain spanning Subgraph of G;
    H in G.allSpanningSG() & the_Vertices_of H = the_Vertices_of G
      by Th60, GLIB_000:def 33;
    hence x in the_Vertices_of G.allSpanningSG() by A2, GLIB_014:def 14;
  end;
  hence thesis by TARSKI:def 1;
end;

theorem
  the_Edges_of G.allSpanningSG() = bool the_Edges_of G
proof
  the_Edges_of G.allSpanningSG() c= the_Edges_of G.allSG()
    by GLIBPRE1:115;
  then A1: the_Edges_of G.allSpanningSG() c= bool the_Edges_of G
    by Th38;
  now
    let x be object;
    reconsider X = x as set by TARSKI:1;
    assume x in bool the_Edges_of G;
    then X c= the_Edges_of G;
    then A2: X c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
    the_Vertices_of G c= the_Vertices_of G;
    then A3: the_Vertices_of G is non empty Subset of the_Vertices_of G;
    set H = the plain inducedSubgraph of G, the_Vertices_of G, X;
    the_Vertices_of H = the_Vertices_of G by A2, A3, GLIB_000:def 37;
    then H is spanning by GLIB_000:def 33;
    then A4: H in G.allSpanningSG() by Th60;
    the_Edges_of H = X by A2, A3, GLIB_000:def 37;
    hence x in the_Edges_of G.allSpanningSG() by A4, GLIB_014:def 15;
  end;
  then bool the_Edges_of G c= the_Edges_of G.allSpanningSG()
    by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

theorem
  G.allInducedSG() /\ G.allSpanningSG() = {G | _GraphSelectors}
proof
  now
    let x be object;
    hereby
      assume x in G.allInducedSG() /\ G.allSpanningSG();
      then A1: x in G.allInducedSG() & x in G.allSpanningSG()
        by XBOOLE_0:def 4;
      then consider V being non empty Subset of the_Vertices_of G such that
        A2: x is plain inducedSubgraph of G, V by Th45;
      reconsider H = x as plain inducedSubgraph of G, V by A2;
      A3: H is spanning by A1, Th60;
      then A4: the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33
        .= V by GLIB_000:def 37;
      the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34
        .= the_Edges_of H by A4, GLIB_000:def 37;
      then G == H & G == G | _GraphSelectors by A3, GLIB_000:128, GLIB_000:118;
      hence x = G | _GraphSelectors by GLIB_000:85, GLIB_009:44;
    end;
    assume x = G | _GraphSelectors;
    then x in G.allInducedSG() & x in G.allSpanningSG()
      by Th47, Th62;
    hence x in G.allInducedSG() /\ G.allSpanningSG()
      by XBOOLE_0:def 4;
  end;
  hence thesis by TARSKI:def 1;
end;

begin :: Forest Subgraph set

definition
  let G;
  func G.allForests() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is acyclic };
  coherence
  proof
    now
      let x be object;
      assume x in { H
        where H is Element of [#]G.allSG() : H is acyclic };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is acyclic;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th78:
  G2 in G1.allForests() iff G2 is plain acyclic Subgraph of G1
proof
  hereby
    assume G2 in G1.allForests();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is acyclic;
    thus G2 is plain acyclic Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain acyclic Subgraph of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th79:
  for H being acyclic Subgraph of G holds H | _GraphSelectors in G.allForests()
proof
  let H be acyclic Subgraph of G;
  H | _GraphSelectors is acyclic Subgraph of G
    by GLIB_000:92, GLIB_002:44, GLIB_000:128;
  hence thesis by Th78;
end;

theorem Th80:
  G is acyclic iff G | _GraphSelectors in G.allForests()
proof
  hereby
    assume A1: G is acyclic;
    G is Subgraph of G by GLIB_000:40;
    hence G | _GraphSelectors in G.allForests() by A1, Th79;
  end;
  assume G | _GraphSelectors in G.allForests();
  then A2: G | _GraphSelectors is acyclic by Th78;
  G | _GraphSelectors == G by GLIB_000:128;
  hence thesis by A2, GLIB_002:44;
end;

theorem Th81:
  for V being non empty Subset of the_Vertices_of G
  holds createGraph(V) in G.allForests() by Th78;

theorem Th82:
  for v being Vertex of G holds createGraph(v) in G.allForests() by Th81;

theorem Th83:
  for G being non edgeless _Graph, e being Edge of G st not e in G.loops()
  holds createGraph(e) in G.allForests()
proof
  let G be non edgeless _Graph, e be Edge of G;
  assume not e in G.loops();
  then createGraph(e) is acyclic by Th18;
  hence thesis by Th78;
end;

theorem Th84:
  for G being non edgeless _Graph, e being Edge of G
  for V being Subset of the_Vertices_of G
  for H being plain addVertices of createGraph(e), V
  st not e in G.loops() holds H in G.allForests()
proof
  let G be non edgeless _Graph, e be Edge of G;
  let V be Subset of the_Vertices_of G;
  let H be plain addVertices of createGraph(e), V;
  assume not e in G.loops();
  then A1: createGraph(e) is acyclic by Th18;
  H is Subgraph of G by Th21;
  hence thesis by A1, Th78;
end;

registration
  let G;
  cluster G.allForests() -> non empty \/-tolerating plain acyclic simple;
  coherence
  proof
    thus G.allForests() is non empty by Th82;
    thus G.allForests() is \/-tolerating plain;
    for H being _Graph st H in G.allForests() holds H is acyclic by Th78;
    hence G.allForests() is acyclic by GLIB_014:def 8;
    hence thesis;
  end;
end;

theorem Th85:
  H.allForests() c= G.allForests()
proof
  now
    let x be object;
    assume x in H.allForests();
    then reconsider H9 = x as plain acyclic Subgraph of H by Th78;
    H9 is Subgraph of G by GLIB_000:43;
    hence x in G.allForests() by Th78;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th86:
  for G2 being loopless _Graph st G2.allForests() c= G1.allForests()
  holds G2 is Subgraph of G1
proof
  let G2 be loopless _Graph;
  assume A1: G2.allForests() c= G1.allForests();
  now
    let x be object;
    assume x in the_Vertices_of G2;
    then reconsider v = x as Vertex of G2;
    createGraph(v) in G2.allForests() by Th82;
    then createGraph(v) is Subgraph of G1 by A1, Th78;
    then the_Vertices_of createGraph(v) c= the_Vertices_of G1
      by GLIB_000:def 32;
    hence x in the_Vertices_of G1 by ZFMISC_1:31;
  end;
  then A2: the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
  A3: the_Edges_of G2 c= the_Edges_of G1
  proof
    per cases;
    suppose G2 is edgeless;
      then the_Edges_of G2 = {};
      hence thesis by XBOOLE_1:2;
    end;
    suppose G2 is non edgeless;
      then reconsider G3 = G2 as non edgeless _Graph;
      now
        let x be object;
        assume x in the_Edges_of G3;
        then reconsider e = x as Edge of G3;
        G2.loops() = {};
        then createGraph(e) in G2.allForests() by Th83;
        then createGraph(e) is Subgraph of G1 by A1, Th78;
        then the_Edges_of createGraph(e) c= the_Edges_of G1 by GLIB_000:def 32;
        then {e} c= the_Edges_of G1 by Th13;
        hence x in the_Edges_of G1 by ZFMISC_1:31;
      end;
      hence thesis by TARSKI:def 3;
    end;
  end;
  now
    let e0 be set;
    assume A4: e0 in the_Edges_of G2;
    then reconsider G3 = G2 as non edgeless _Graph;
    reconsider e = e0 as Edge of G3 by A4;
    G2.loops() = {};
    then createGraph(e) in G2.allForests() by Th83;
    then A5: createGraph(e) is Subgraph of G1 by A1, Th78;
    the_Edges_of createGraph(e) = {e} by Th13;
    then A6: e0 in the_Edges_of createGraph(e) by TARSKI:def 1;
    then (the_Source_of createGraph(e)).e0 = (the_Source_of G1).e0 &
      (the_Target_of createGraph(e)).e0 = (the_Target_of G1).e0
      by A5, GLIB_000:def 32;
    hence (the_Source_of G2).e0 = (the_Source_of G1).e0 &
      (the_Target_of G2).e0 = (the_Target_of G1).e0 by A6, GLIB_000:def 32;
  end;
  hence thesis by A2, A3, GLIB_000:def 32;
end;

theorem Th87:
  for H being removeLoops of G holds G.allForests() = H.allForests()
proof
  let H be removeLoops of G;
  A1: H.allForests() c= G.allForests() by Th85;
  now
    let z be object;
    assume z in G.allForests();
    then reconsider H9 = z as plain acyclic Subgraph of G by Th78;
    the_Vertices_of H9 c= the_Vertices_of G;
    then A2: the_Vertices_of H9 c= the_Vertices_of H by GLIB_000:def 33;
    now
      let x be object;
      assume A3: x in the_Edges_of H9;
      then A4: x in the_Edges_of G;
      not x in G.loops()
      proof
        assume x in G.loops();
        then consider v being object such that
          A5: x Joins v,v,G by GLIB_009:def 2;
        x is set & v is set by TARSKI:1;
        then x Joins v,v,H9 by A3, A5, GLIB_000:73;
        then x in H9.loops() by GLIB_009:def 2;
        hence contradiction;
      end;
      then x in the_Edges_of G \ G.loops() by A4, XBOOLE_0:def 5;
      hence x in the_Edges_of H by GLIB_000:53;
    end;
    then the_Edges_of H9 c= the_Edges_of H by TARSKI:def 3;
    then H9 is Subgraph of H by A2, GLIB_000:44;
    hence z in H.allForests() by Th78;
  end;
  then G.allForests() c= H.allForests() by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

theorem Th88:
  for G1, G2 being loopless _Graph
  holds G1 == G2 iff G1.allForests() = G2.allForests()
proof
  let G1, G2 be loopless _Graph;
  hereby
    assume G1 == G2;
    then G2 is removeLoops of G1 by GLIB_009:58;
    hence G1.allForests() = G2.allForests() by Th87;
  end;
  assume G1.allForests() = G2.allForests();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th86;
  hence thesis by GLIB_000:87;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G3 == G4 iff G1.allForests() = G2.allForests()
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  hereby
    assume A1: G3 == G4;
    thus G1.allForests() = G3.allForests() by Th87
      .= G4.allForests() by A1, Th88
      .= G2.allForests() by Th87;
  end;
  assume A2: G1.allForests() = G2.allForests();
  G3.allForests() = G1.allForests() by Th87
    .= G4.allForests() by A2, Th87;
  hence thesis by Th88;
end;

theorem Th90:
  for F being PGraphMapping of G1, G2 st F is weak_SG-embedding
  holds rng(SG2SGFunc(F) | G1.allForests()) c= G2.allForests()
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is weak_SG-embedding;
  set f = SG2SGFunc(F) | G1.allForests();
  now
    let y be object;
    assume A2: y in rng f;
    then consider x being object such that
      A3: x in dom f & f.x = y by FUNCT_1:def 3;
    reconsider H1 = x as plain acyclic Subgraph of G1 by A3, Th78;
    y in rng SG2SGFunc(F) by A2, TARSKI:def 3, RELAT_1:70;
    then reconsider H2 = y as plain Subgraph of G2 by Th1;
    A4: H2 = (SG2SGFunc F).x by A3, FUNCT_1:47
      .= rng(F|H1) by Def5;
    H2 is acyclic
    proof
      assume H2 is non acyclic;
      :: show that a cycle in H2 comes from a cycle in H1
      then consider W2 being Walk of H2 such that
        A5: W2 is Cycle-like by GLIB_002:def 2;
      dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
      then A6: the_Vertices_of H1 c= dom F_V;
      dom((F|H1)_V) = the_Vertices_of H1 by A6, RELAT_1:62;
      then reconsider F9 = F|H1 as non empty one-to-one PGraphMapping of H1, G2
        by A1;
      rng(F9_V) = the_Vertices_of H2 by A4, GLIB_010:54;
      then A7: W2.vertices() c= rng(F9_V);
      rng(F9_E) = the_Edges_of H2 by A4, GLIB_010:54;
      then A8: W2.edges() c= rng(F9_E);
      reconsider W0 = W2 as Walk of G2 by GLIB_001:167;
      W0.edges() = W2.edges() & W0.vertices() = W2.vertices()
        by GLIB_001:98, GLIB_001:110;
      then reconsider W2 as F9-valued Walk of G2 by A7, A8, GLIB_010:def 36;
      W2 is Cycle-like by A5, GLIB_006:24;
      then F9"W2 is Cycle-like by GLIB_010:138;
      hence contradiction by GLIB_002:def 2;
    end;
    hence y in G2.allForests() by Th78;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th91:
  for F being PGraphMapping of G1, G2 st F is one-to-one onto
  holds G2.allForests() c= rng(SG2SGFunc(F) | G1.allForests())
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is one-to-one onto;
  set f = SG2SGFunc(F) | G1.allForests();
  A2: dom f = G1.allForests() by FUNCT_2:def 1;
  now
    let x be object;
    assume x in G2.allForests();
    then reconsider H2 = x as plain acyclic Subgraph of G2 by Th78;
    rng F == G2 by A1, GLIB_010:56;
    then A3: H2 is Subgraph of rng F by GLIB_000:91;
    set H1 = the plain inducedSubgraph of
      G1, F_V"the_Vertices_of H2, F_E"the_Edges_of H2;
    H1 is acyclic by A1, A3, GLIBPRE1:107;
    then A4: H1 in dom f by A2, Th78;
    A5: rng(F | H1) = H2 by A1, A3, GLIB_009:44, GLIBPRE1:99;
    f.H1 = SG2SGFunc(F).H1 by A4, FUNCT_1:47
      .= H2 by A5, Def5;
    hence x in rng f by A4, FUNCT_1:3;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th92:
  for F being PGraphMapping of G1, G2 st F is isomorphism
  holds G2.allForests() = rng(SG2SGFunc(F) | G1.allForests())
proof
  let F be PGraphMapping of G1, G2;
  assume F is isomorphism;
  then rng(SG2SGFunc(F) | G1.allForests()) c= G2.allForests() &
    G2.allForests() c= rng(SG2SGFunc(F) | G1.allForests())
    by Th90, Th91;
  hence thesis by XBOOLE_0:def 10;
end;

theorem Th93:
  G2 is G1-Disomorphic implies G1.allForests(),G2.allForests() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allForests();
  A2: dom f = G1.allForests() by FUNCT_2:def 1;
  A3: rng f = G2.allForests() by A1, Th92;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allForests();
    then reconsider H = G as plain acyclic Subgraph of G1 by Th78;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem Th94:
  G2 is G1-isomorphic implies G1.allForests(),G2.allForests() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allForests();
  A2: dom f = G1.allForests() by FUNCT_2:def 1;
  A3: rng f = G2.allForests() by A1, Th92;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allForests();
    then reconsider H = G as plain acyclic Subgraph of G1 by Th78;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  st G4 is G3-Disomorphic holds G1.allForests(),G2.allForests() are_Disomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allForests() = G3.allForests() & G2.allForests()=G4.allForests() by Th87;
  hence thesis by Th93;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  st G4 is G3-isomorphic holds G1.allForests(),G2.allForests() are_isomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allForests() = G3.allForests() & G2.allForests()=G4.allForests() by Th87;
  hence thesis by Th94;
end;

theorem Th97:
  for H being removeLoops of G holds H is GraphUnion of G.allForests()
proof
  let H be removeLoops of G;
  set G9 = the GraphUnion of G.allForests();
  reconsider G8 = G as GraphUnion of G.allSG() by Th35;
  set H9 = the GraphUnion of {H};
  now
    thus G9 is Subgraph of G8 by GLIBPRE1:119;
    now
      let x be object;
      assume x in the_Vertices_of H;
      then reconsider v = x as Vertex of G;
      set H8 = createGraph(v);
      H8 in G.allForests() by Th82;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Vertices_of H8 c= the_Vertices_of G9 by GLIB_000:def 32;
      hence x in the_Vertices_of G9 by ZFMISC_1:31;
    end;
    hence the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;
    now
      let x be object;
      assume x in the_Edges_of H;
      then x in the_Edges_of G \ G.loops() by GLIB_000:53;
      then A1: x in the_Edges_of G & not x in G.loops() by XBOOLE_0:def 5;
      then reconsider G0 = G as non edgeless _Graph;
      reconsider e = x as Edge of G0 by A1;
      set H8 = createGraph(e);
      H8 in G.allForests() by A1, Th83;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Edges_of H8 c= the_Edges_of G9 by GLIB_000:def 32;
      then {e} c= the_Edges_of G9 by Th13;
      hence x in the_Edges_of G9 by ZFMISC_1:31;
    end;
    hence the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;
  end;
  then A2: H is Subgraph of G9 by GLIB_000:44;
  now
    let H2 be Element of G.allForests();
    reconsider H1 = H as Element of {H} by TARSKI:def 1;
    take H1;
    H.allForests() = G.allForests() by Th87;
    hence H2 is Subgraph of H1 by Th78;
  end;
  then G9 is Subgraph of H9 by GLIBPRE1:118;
  then G9 is Subgraph of H by GLIB_000:91, GLIB_014:24;
  hence thesis by A2, GLIB_000:87, GLIB_014:22;
end;

theorem
  G is loopless iff G is GraphUnion of G.allForests()
proof
  hereby
    set H = the removeLoops of G;
    assume G is loopless;
    then A1: G == H by GLIB_009:58;
    H is GraphUnion of G.allForests() by Th97;
    hence G is GraphUnion of G.allForests() by A1, GLIB_014:22;
  end;
  assume G is GraphUnion of G.allForests();
  hence G is loopless;
end;

theorem Th99:
  the_Edges_of G = G.loops() iff G.allForests() is edgeless
proof
  hereby
    set H = the removeLoops of G;
    assume A1: the_Edges_of G = G.loops();
    now
      let H be _Graph;
      assume H in G.allForests();
      then A2: H is acyclic Subgraph of G by Th78;
      now
        assume the_Edges_of H <> {};
        then consider e being object such that
          A3: e in the_Edges_of H by XBOOLE_0:def 1;
        the_Edges_of H c= the_Edges_of G by A2, GLIB_000:def 32;
        then consider v being object such that
          A4: e Joins v,v,G by A1, A3, GLIB_009:def 2;
        e is set & v is set by TARSKI:1;
        then e Joins v,v,H by A2, A3, A4, GLIB_000:73;
        hence contradiction by A2, GLIB_000:18;
      end;
      hence H is edgeless;
    end;
    hence G.allForests() is edgeless by GLIB_014:def 12;
  end;
  assume A5: G.allForests() is edgeless;
  now
    let x be object;
    assume A6: x in the_Edges_of G;
    then reconsider G9 = G as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A6;
    set H9 = createGraph(e);
    assume not x in G.loops();
    then H9 in G.allForests() by Th83;
    hence contradiction by A5;
  end;
  then the_Edges_of G c= G.loops() by TARSKI:def 3;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  the_Edges_of G = G.loops() iff G.allForests() = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G
proof
  set S = the set of all createGraph(V)
    where V is non empty Subset of the_Vertices_of G;
  hereby
    assume the_Edges_of G = G.loops();
    then A1: G.allForests() is edgeless by Th99;
    now
      let x be object;
      hereby
        assume A2: x in G.allForests();
        then reconsider H = x as plain Subgraph of G by Th78;
        reconsider V = the_Vertices_of H as non empty Subset of
          the_Vertices_of G;
        set H9 = createGraph(V);
        reconsider H9 as plain Subgraph of G;
        A3: the_Vertices_of H = the_Vertices_of H9;
        the_Edges_of H = the_Edges_of H9 by A1, A2;
        then H is Subgraph of H9 & H9 is Subgraph of H by A3, GLIB_000:44;
        then H = H9 by GLIB_000:87, GLIB_009:44;
        hence x in S;
      end;
      assume x in S;
      then consider V being non empty Subset of the_Vertices_of G such that
        A4: x = createGraph(V);
      thus x in G.allForests() by A4, Th81;
    end;
    hence G.allForests() = S by TARSKI:2;
  end;
  assume A5: G.allForests() = S;
  now
    let H be _Graph;
    assume H in G.allForests();
    then consider V being non empty Subset of the_Vertices_of G such that
      A6: H = createGraph(V) by A5;
    thus H is edgeless by A6;
  end;
  then G.allForests() is edgeless by GLIB_014:def 12;
  hence thesis by Th99;
end;

theorem
  the_Vertices_of G.allForests() = (bool the_Vertices_of G) \ {{}}
proof
  the_Vertices_of G.allForests() c= the_Vertices_of G.allSG() by GLIBPRE1:115;
  then A1: the_Vertices_of G.allForests() c= (bool the_Vertices_of G) \ {{}}
    by Th37;
  now
    let x be object;
    reconsider X = x as set by TARSKI:1;
    assume x in (bool the_Vertices_of G) \ {{}};
    then x in bool the_Vertices_of G & not x in {{}} by XBOOLE_0:def 5;
    then reconsider X as non empty Subset of the_Vertices_of G by TARSKI:def 1;
    set H = createGraph(X);
    the_Vertices_of H = X & H in G.allForests() by Th81;
    hence x in the_Vertices_of G.allForests() by GLIB_014:def 14;
  end;
  then (bool the_Vertices_of G) \ {{}} c= the_Vertices_of G.allForests()
    by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

begin :: Spanning Forest Subgraph set

definition
  let G;
  func G.allSpanningForests() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is spanning acyclic };
  coherence
  proof
    now
      let x be object;
      assume x in { H
        where H is Element of [#]G.allSG() : H is spanning acyclic };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is spanning acyclic;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th102:
  G2 in G1.allSpanningForests() iff G2 is plain spanning acyclic Subgraph of G1
proof
  hereby
    assume G2 in G1.allSpanningForests();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is spanning acyclic;
    thus G2 is plain spanning acyclic Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain spanning acyclic Subgraph of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th103:
  G.allSpanningForests() = G.allSpanningSG() /\ G.allForests()
proof
  now
    let x be object;
    hereby
      assume x in G.allSpanningForests();
      then x is plain spanning acyclic Subgraph of G by Th102;
      hence x in G.allSpanningSG() & x in G.allForests() by Th60, Th78;
    end;
    assume x in G.allSpanningSG() & x in G.allForests();
    then x is plain spanning Subgraph of G & x is plain acyclic Subgraph of G
      by Th60;
    hence x in G.allSpanningForests() by Th102;
  end;
  hence thesis by XBOOLE_0:def 4;
end;

theorem Th104:
  for H being spanning acyclic Subgraph of G
  holds H | _GraphSelectors in G.allSpanningForests()
proof
  let H be spanning acyclic Subgraph of G;
  H | _GraphSelectors == H by GLIB_000:128;
  then H | _GraphSelectors is spanning acyclic Subgraph of G
    by GLIB_000:171, GLIB_002:44;
  hence thesis by Th102;
end;

theorem
  G is acyclic iff G | _GraphSelectors in G.allSpanningForests()
proof
  A1: G.allSpanningForests() = G.allSpanningSG() /\ G.allForests()
    by Th103;
  hereby
    assume G is acyclic;
    then A2: G | _GraphSelectors in G.allForests() by Th80;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    hence G | _GraphSelectors in G.allSpanningForests()
      by A1, A2, XBOOLE_0:def 4;
  end;
  assume G | _GraphSelectors in G.allSpanningForests();
  then G | _GraphSelectors in G.allForests() by A1;
  hence G is acyclic by Th80;
end;

theorem Th106:
  createGraph([#]the_Vertices_of G) in G.allSpanningForests()
proof
  set H = createGraph([#]the_Vertices_of G);
  A1: H in G.allForests() by Th81;
  A2: H in G.allSpanningSG() by Th63;
  G.allSpanningForests() = G.allSpanningSG() /\ G.allForests() by Th103;
  hence thesis by A1, A2, XBOOLE_0:def 4;
end;

theorem Th107:
  for G being non edgeless _Graph, e being Edge of G
  for H being plain addVertices of createGraph(e), the_Vertices_of G
  st not e in G.loops() holds H in G.allSpanningForests()
proof
  let G be non edgeless _Graph, e be Edge of G;
  let H be plain addVertices of createGraph(e), the_Vertices_of G;
  assume A1: not e in G.loops();
  the_Vertices_of G c= the_Vertices_of G;
  then H in G.allForests() & H in G.allSpanningSG() by A1, Th64, Th84;
  then H in G.allForests() /\ G.allSpanningSG() by XBOOLE_0:def 4;
  hence thesis by Th103;
end;

registration
  let G;
  cluster G.allSpanningForests() -> non empty \/-tolerating plain acyclic
    simple;
  coherence
  proof
    thus G.allSpanningForests() is non empty by Th106;
    G.allSpanningForests() = G.allSpanningSG() /\ G.allForests() by Th103;
    hence thesis;
  end;
end;

theorem Th108:
  for H being spanning Subgraph of G
  holds H.allSpanningForests() c= G.allSpanningForests()
proof
  let H be spanning Subgraph of G;
  now
    let x be object;
    assume x in H.allSpanningForests();
    then reconsider H9 = x as plain spanning acyclic Subgraph of H by Th102;
    the_Vertices_of H9 = the_Vertices_of H by GLIB_000:def 33
      .= the_Vertices_of G by GLIB_000:def 33;
    then H9 is plain spanning acyclic Subgraph of G
      by GLIB_000:43, GLIB_000:def 33;
    hence x in G.allSpanningForests() by Th102;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th109:
  for G2 being loopless _Graph
  holds G2.allSpanningForests() c= G1.allSpanningForests()
  implies G2 is spanning Subgraph of G1
proof
  let G2 be loopless _Graph;
  assume A1: G2.allSpanningForests() c= G1.allSpanningForests();
  set H0 = the plain spanning acyclic Subgraph of G2;
  H0 in G2.allSpanningForests() by Th102;
  then H0 is spanning Subgraph of G1 by A1, Th102;
  then A2: the_Vertices_of G1 = the_Vertices_of H0 by GLIB_000:def 33
    .= the_Vertices_of G2 by GLIB_000:def 33;
  now
    let x be object;
    assume A3: x in the_Edges_of G2;
    then reconsider G9 = G2 as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A3;
    set H = the plain addVertices of createGraph(e), the_Vertices_of G2;
    not e in G9.loops();
    then H in G2.allSpanningForests() by Th107;
    then H is Subgraph of G1 by A1, Th102;
    then the_Edges_of H c= the_Edges_of G1 by GLIB_000:def 32;
    then the_Edges_of createGraph(e) c= the_Edges_of G1 by GLIB_006:def 10;
    then {e} c= the_Edges_of G1 by Th13;
    hence x in the_Edges_of G1 by ZFMISC_1:31;
  end;
  then A4: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
  now
    let x be set;
    assume A5: x in the_Edges_of G2;
    then reconsider G9 = G2 as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A5;
    set H = the plain addVertices of createGraph(e), the_Vertices_of G2;
    not e in G9.loops();
    then H in G2.allSpanningForests() by Th107;
    then A6: H is Subgraph of G1 & H is Subgraph of G2 by A1, Th102;
    the_Edges_of H = the_Edges_of createGraph(e) by GLIB_006:def 10
      .= {e} by Th13;
    then A7: x in the_Edges_of H by TARSKI:def 1;
    thus (the_Source_of G2).x = (the_Source_of H).x by A6, A7, GLIB_000:def 32
      .= (the_Source_of G1).x by A6, A7, GLIB_000:def 32;
    thus (the_Target_of G2).x = (the_Target_of H).x by A6, A7, GLIB_000:def 32
      .= (the_Target_of G1).x by A6, A7, GLIB_000:def 32;
  end;
  hence thesis by A2, A4, GLIB_000:def 32, GLIB_000:def 33;
end;

theorem Th110:
  for H being removeLoops of G
  holds G.allSpanningForests() = H.allSpanningForests()
proof
  let H be removeLoops of G;
  A1: H.allSpanningForests() c= G.allSpanningForests() by Th108;
  now
    let z be object;
    assume z in G.allSpanningForests();
    then reconsider H9 = z as plain acyclic spanning Subgraph of G by Th102;
    A2: the_Vertices_of H9 = the_Vertices_of G by GLIB_000:def 33
      .= the_Vertices_of H by GLIB_000:def 33;
    now
      let x be object;
      assume A3: x in the_Edges_of H9;
      then A4: x in the_Edges_of G;
      not x in G.loops()
      proof
        assume x in G.loops();
        then consider v being object such that
          A5: x Joins v,v,G by GLIB_009:def 2;
        x is set & v is set by TARSKI:1;
        then x Joins v,v,H9 by A3, A5, GLIB_000:73;
        then x in H9.loops() by GLIB_009:def 2;
        hence contradiction;
      end;
      then x in the_Edges_of G \ G.loops() by A4, XBOOLE_0:def 5;
      hence x in the_Edges_of H by GLIB_000:53;
    end;
    then the_Edges_of H9 c= the_Edges_of H by TARSKI:def 3;
    then H9 is spanning Subgraph of H by A2, GLIB_000:44, GLIB_000:def 33;
    hence z in H.allSpanningForests() by Th102;
  end;
  then G.allSpanningForests() c= H.allSpanningForests() by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

theorem Th111:
  for G1, G2 being loopless _Graph
  holds G1 == G2 iff G1.allSpanningForests() = G2.allSpanningForests()
proof
  let G1, G2 be loopless _Graph;
  hereby
    assume G1 == G2;
    then G2 is removeLoops of G1 by GLIB_009:58;
    hence G1.allSpanningForests() = G2.allSpanningForests() by Th110;
  end;
  assume G1.allSpanningForests() = G2.allSpanningForests();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th109;
  hence thesis by GLIB_000:87;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G3 == G4 iff G1.allSpanningForests() = G2.allSpanningForests()
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  hereby
    assume A1: G3 == G4;
    thus G1.allSpanningForests() = G3.allSpanningForests() by Th110
      .= G4.allSpanningForests() by A1, Th111
      .= G2.allSpanningForests() by Th110;
  end;
  assume A2: G1.allSpanningForests() = G2.allSpanningForests();
  G3.allSpanningForests() = G1.allSpanningForests() by Th110
    .= G4.allSpanningForests() by A2, Th110;
  hence thesis by Th111;
end;

theorem Th113:
  for F being PGraphMapping of G1, G2
  st F is weak_SG-embedding & rng F_V = the_Vertices_of G2
  holds rng(SG2SGFunc(F) | G1.allSpanningForests()) c= G2.allSpanningForests()
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  assume F is weak_SG-embedding & rng F_V = the_Vertices_of G2;
  then A1: rng(f | G1.allForests()) c= G2.allForests() &
    rng(f | G1.allSpanningSG()) c= G2.allSpanningSG()
    by Th67, Th90;
  f | G1.allSpanningForests()
     = f | (G1.allSpanningSG() /\ G1.allForests()) by Th103
    .= (f | G1.allSpanningSG()) /\ (f | G1.allForests()) by RELAT_1:79;
  then A2: rng(f | G1.allSpanningForests()) c=
    rng(f|G1.allSpanningSG())/\rng(f|G1.allForests()) by RELAT_1:13;
  rng(f|G1.allSpanningSG())/\rng(f|G1.allForests()) c=
    G2.allSpanningSG() /\ G2.allForests() by A1, XBOOLE_1:27;
  then rng(f | G1.allSpanningForests()) c=
    G2.allSpanningSG() /\ G2.allForests() by A2, XBOOLE_1:1;
  hence thesis by Th103;
end;

theorem Th114:
  for F being PGraphMapping of G1, G2 st F is weak_SG-embedding onto
  holds G2.allSpanningForests() = rng(SG2SGFunc(F) | G1.allSpanningForests())
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  assume A1: F is weak_SG-embedding onto;
  then rng F_V = the_Vertices_of G2 by GLIB_010:def 12;
  then A2: rng(f | G1.allSpanningForests()) c= G2.allSpanningForests()
    by A1, Th113;
  dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
  then F_V is total by PARTFUN1:def 2;
  then G2.allForests() c= rng(f | G1.allForests()) &
    G2.allSpanningSG() c= rng(f | G1.allSpanningSG())
    by A1, Th68, Th91;
  then G2.allForests() /\ G2.allSpanningSG() c=
    rng(f | G1.allForests()) /\ rng(f | G1.allSpanningSG())
    by XBOOLE_1:27;
  then A3: G2.allSpanningForests() c=
    rng(f | G1.allForests()) /\ rng(f | G1.allSpanningSG()) by Th103;
  A4: rng(f | G1.allForests()) = f.:G1.allForests() by RELAT_1:115;
  A5: rng(f | G1.allSpanningSG()) = f.:G1.allSpanningSG()
    by RELAT_1:115;
  A6: f is one-to-one by A1, Th31;
  rng(f | G1.allForests()) /\ rng(f | G1.allSpanningSG())
     = f.:(G1.allForests() /\ G1.allSpanningSG()) by A4, A5, A6, FUNCT_1:62
    .= rng(f | (G1.allForests() /\ G1.allSpanningSG())) by RELAT_1:115
    .= rng(f | G1.allSpanningForests()) by Th103;
  hence thesis by A2, A3, XBOOLE_0:def 10;
end;

theorem Th115:
  for G1, G2 being _Graph holds G2 is G1-Disomorphic implies
    G1.allSpanningForests(),G2.allSpanningForests() are_Disomorphic
proof
  let G1, G2 be _Graph;
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allSpanningForests();
  A2: dom f = G1.allSpanningForests() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningForests() by A1, Th114;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningForests();
    then reconsider H = G as plain spanning acyclic Subgraph of G1 by Th102;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem Th116:
  for G1, G2 being _Graph holds G2 is G1-isomorphic implies
    G1.allSpanningForests(),G2.allSpanningForests() are_isomorphic
proof
  let G1, G2 be _Graph;
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allSpanningForests();
  A2: dom f = G1.allSpanningForests() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningForests() by A1, Th114;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningForests();
    then reconsider H = G as plain spanning acyclic Subgraph of G1 by Th102;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-Disomorphic implies
    G1.allSpanningForests(),G2.allSpanningForests() are_Disomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allSpanningForests() = G3.allSpanningForests() &
    G2.allSpanningForests() = G4.allSpanningForests() by Th110;
  hence thesis by Th115;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-isomorphic implies
    G1.allSpanningForests(),G2.allSpanningForests() are_isomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allSpanningForests() = G3.allSpanningForests() &
    G2.allSpanningForests() = G4.allSpanningForests() by Th110;
  hence thesis by Th116;
end;

theorem Th119:
  for H being removeLoops of G holds H is GraphUnion of G.allSpanningForests()
proof
  let H be removeLoops of G;
  set G9 = the GraphUnion of G.allSpanningForests();
  reconsider G8 = G as GraphUnion of G.allSG() by Th35;
  set H9 = the GraphUnion of {H};
  now
    thus G9 is Subgraph of G8 by GLIBPRE1:119;
    now
      let x be object;
      assume x in the_Vertices_of H;
      then A1: x in the_Vertices_of G;
      set H8 = createGraph([#]the_Vertices_of G);
      H8 in G.allSpanningForests() by Th106;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Vertices_of H8 c= the_Vertices_of G9 by GLIB_000:def 32;
      hence x in the_Vertices_of G9 by A1;
    end;
    hence the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;
    now
      let x be object;
      assume x in the_Edges_of H;
      then x in the_Edges_of G \ G.loops() by GLIB_000:53;
      then A2: x in the_Edges_of G & not x in G.loops() by XBOOLE_0:def 5;
      then reconsider G0 = G as non edgeless _Graph;
      reconsider e = x as Edge of G0 by A2;
      set H8 = the plain addVertices of createGraph(e), the_Vertices_of G;
      H8 in G.allSpanningForests() by A2, Th107;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Edges_of H8 c= the_Edges_of G9 by GLIB_000:def 32;
      then the_Edges_of createGraph(e) c= the_Edges_of G9 by GLIB_006:def 10;
      then {e} c= the_Edges_of G9 by Th13;
      hence x in the_Edges_of G9 by ZFMISC_1:31;
    end;
    hence the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;
  end;
  then A3: H is Subgraph of G9 by GLIB_000:44;
  now
    let H2 be Element of G.allSpanningForests();
    reconsider H1 = H as Element of {H} by TARSKI:def 1;
    take H1;
    H.allSpanningForests() = G.allSpanningForests() by Th110;
    hence H2 is Subgraph of H1 by Th102;
  end;
  then G9 is Subgraph of H9 by GLIBPRE1:118;
  then G9 is Subgraph of H by GLIB_000:91, GLIB_014:24;
  hence thesis by A3, GLIB_000:87, GLIB_014:22;
end;

theorem
  G is loopless iff G is GraphUnion of G.allSpanningForests()
proof
  hereby
    set H = the removeLoops of G;
    assume G is loopless;
    then A1: G == H by GLIB_009:58;
    H is GraphUnion of G.allSpanningForests() by Th119;
    hence G is GraphUnion of G.allSpanningForests() by A1, GLIB_014:22;
  end;
  assume G is GraphUnion of G.allSpanningForests();
  hence G is loopless;
end;

theorem
  the_Edges_of G = G.loops() iff G.allSpanningForests() is edgeless
proof
  hereby
    assume the_Edges_of G = G.loops();
    then A1: G.allForests() is edgeless by Th99;
    G.allSpanningForests() = G.allSpanningSG() /\ G.allForests() by Th103;
    hence G.allSpanningForests() is edgeless by A1;
  end;
  assume A2: G.allSpanningForests() is edgeless;
  now
    let x be object;
    assume A3: x in the_Edges_of G;
    then reconsider G9 = G as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A3;
    set H9 = the plain addVertices of createGraph(e), the_Vertices_of G;
    assume not x in G.loops();
    then H9 in G.allSpanningForests() by Th107;
    hence contradiction by A2;
  end;
  then the_Edges_of G c= G.loops() by TARSKI:def 3;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  the_Edges_of G = G.loops() iff for H being removeLoops of G
    holds G.allSpanningForests() = {H | _GraphSelectors}
proof
  hereby
    assume A1: the_Edges_of G = G.loops();
    let H be removeLoops of G;
    A2: H is edgeless by A1;
    now
      let x be object;
      hereby
        assume x in G.allSpanningForests();
        then reconsider H9 = x as plain spanning acyclic Subgraph of G by Th102
;
        now
          thus the_Vertices_of H9 = the_Vertices_of G by GLIB_000:def 33
            .= the_Vertices_of H by GLIB_000:def 33;
          A3: the_Edges_of H9 = {}
          proof
            assume the_Edges_of H9 <> {};
            then consider e being object such that
              A4: e in the_Edges_of H9 by XBOOLE_0:def 1;
            set v = (the_Source_of H9).e, w = (the_Target_of H9).e;
            A5: e Joins v,w,H9 by A4, GLIB_000:def 13;
            per cases;
            suppose v = w;
              then H9.walkOf(v,e,w) is Cycle-like by A5, GLIB_001:156;
              hence contradiction by GLIB_002:def 2;
            end;
            suppose A6: v <> w;
              e Joins v,w,G by A5, GLIB_000:72;
              hence contradiction by A1, A4, A6, GLIB_009:46;
            end;
          end;
          hence the_Edges_of H9 = the_Edges_of H by A2;
          hence the_Source_of H9 = the_Source_of H &
            the_Target_of H9 = the_Target_of H by A3;
        end;
        then A7: H9 == H by GLIB_000:def 34;
        H == H | _GraphSelectors by GLIB_000:128;
        hence x = H | _GraphSelectors by A7, GLIB_000:85, GLIB_009:44;
      end;
      assume x = H | _GraphSelectors;
      hence x in G.allSpanningForests() by A2, Th104;
    end;
    hence G.allSpanningForests() = {H | _GraphSelectors} by TARSKI:def 1;
  end;
  assume A8: for H being removeLoops of G
    holds G.allSpanningForests() = {H | _GraphSelectors};
  now
    let e be object;
    assume A9: e in the_Edges_of G & not e in G.loops();
    set H = the removeLoops of G, H9 = the removeEdges of G, the_Edges_of G;
    A10: H == H | _GraphSelectors & H9 == H9 | _GraphSelectors by GLIB_000:128;
    the_Edges_of H = the_Edges_of G \ G.loops() by GLIB_000:53;
    then e in the_Edges_of H by A9, XBOOLE_0:def 5;
    then A11: e in the_Edges_of (H | _GraphSelectors) by A10, GLIB_000:def 34;
    not e in the_Edges_of H9;
    then not e in the_Edges_of (H9 | _GraphSelectors) by A10, GLIB_000:def 34;
    then A12: H | _GraphSelectors <> H9 | _GraphSelectors by A11;
    A13: H | _GraphSelectors in {H | _GraphSelectors} by TARSKI:def 1;
    H9 | _GraphSelectors in G.allSpanningForests() by Th104;
    then H9 | _GraphSelectors in {H | _GraphSelectors} by A8;
    then {H | _GraphSelectors, H9 | _GraphSelectors} c= {H | _GraphSelectors}
      by A13, ZFMISC_1:32;
    hence contradiction by A12, ZFMISC_1:20;
  end;
  then the_Edges_of G c= G.loops() by TARSKI:def 3;
  hence thesis by XBOOLE_0:def 10;
end;

theorem Th123:
  the_Vertices_of G.allSpanningForests() = { the_Vertices_of G }
proof
  G.allSpanningForests() = G.allSpanningSG() /\ G.allForests() by Th103;
  then G.allSpanningForests() c= G.allSpanningSG() by XBOOLE_1:17;
  then the_Vertices_of G.allSpanningForests() c=
    the_Vertices_of G.allSpanningSG() by GLIBPRE1:115;
  then the_Vertices_of G.allSpanningForests() c= {the_Vertices_of G} by Th75;
  hence thesis by ZFMISC_1:33;
end;

begin :: Connected Subgraph set

definition
  let G;
  func G.allConnectedSG() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is connected };
  coherence
  proof
    now
      let x be object;
      assume x in { H where H is Element of [#]G.allSG() : H is connected };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is connected;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th124:
  G2 in G1.allConnectedSG() iff G2 is plain connected Subgraph of G1
proof
  hereby
    assume G2 in G1.allConnectedSG();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is connected;
    thus G2 is plain connected Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain connected Subgraph of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th125:
  for H being connected Subgraph of G
  holds H | _GraphSelectors in G.allConnectedSG()
proof
  let H be connected Subgraph of G;
  H | _GraphSelectors is connected Subgraph of G
    by GLIB_000:92, GLIB_002:8, GLIB_000:128;
  hence thesis by Th124;
end;

theorem
  G is connected iff G | _GraphSelectors in G.allConnectedSG()
proof
  hereby
    assume A1: G is connected;
    G is Subgraph of G by GLIB_000:40;
    hence G | _GraphSelectors in G.allConnectedSG() by A1, Th125;
  end;
  assume G | _GraphSelectors in G.allConnectedSG();
  then A2: G | _GraphSelectors is connected by Th124;
  G | _GraphSelectors == G by GLIB_000:128;
  hence thesis by A2, GLIB_002:8;
end;

theorem Th127:
  for v being Vertex of G holds createGraph(v) in G.allConnectedSG() by Th124;

theorem Th128:
  for G being non edgeless _Graph, e being Edge of G
  holds createGraph(e) in G.allConnectedSG() by Th124;

registration
  let G;
  cluster G.allConnectedSG() -> non empty \/-tolerating plain connected;
  coherence
  proof
    thus G.allConnectedSG() is non empty by Th127;
    thus G.allConnectedSG() is \/-tolerating plain;
    for H being _Graph st H in G.allConnectedSG() holds H is connected by Th124
;
    hence G.allConnectedSG() is connected by GLIB_014:def 9;
  end;
end;

theorem Th129:
  H.allConnectedSG() c= G.allConnectedSG()
proof
  now
    let x be object;
    assume x in H.allConnectedSG();
    then reconsider H9 = x as plain connected Subgraph of H by Th124;
    H9 is Subgraph of G by GLIB_000:43;
    hence x in G.allConnectedSG() by Th124;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th130:
  G2.allConnectedSG() c= G1.allConnectedSG() implies G2 is Subgraph of G1
proof
  assume A1: G2.allConnectedSG() c= G1.allConnectedSG();
  now
    let x be object;
    assume x in the_Vertices_of G2;
    then reconsider v = x as Vertex of G2;
    createGraph(v) in G2.allConnectedSG() by Th127;
    then createGraph(v) is Subgraph of G1 by A1, Th124;
    then the_Vertices_of createGraph(v) c= the_Vertices_of G1
      by GLIB_000:def 32;
    hence x in the_Vertices_of G1 by ZFMISC_1:31;
  end;
  then A2: the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
  A3: the_Edges_of G2 c= the_Edges_of G1
  proof
    per cases;
    suppose G2 is edgeless;
      then the_Edges_of G2 = {};
      hence thesis by XBOOLE_1:2;
    end;
    suppose G2 is non edgeless;
      then reconsider G3 = G2 as non edgeless _Graph;
      now
        let x be object;
        assume x in the_Edges_of G3;
        then reconsider e = x as Edge of G3;
        createGraph(e) in G2.allConnectedSG() by Th128;
        then createGraph(e) is Subgraph of G1 by A1, Th124;
        then the_Edges_of createGraph(e) c= the_Edges_of G1 by GLIB_000:def 32;
        then {e} c= the_Edges_of G1 by Th13;
        hence x in the_Edges_of G1 by ZFMISC_1:31;
      end;
      hence thesis by TARSKI:def 3;
    end;
  end;
  now
    let e0 be set;
    assume A4: e0 in the_Edges_of G2;
    then reconsider G3 = G2 as non edgeless _Graph;
    reconsider e = e0 as Edge of G3 by A4;
    createGraph(e) in G2.allConnectedSG() by Th128;
    then A5: createGraph(e) is Subgraph of G1 by A1, Th124;
    the_Edges_of createGraph(e) = {e} by Th13;
    then A6: e0 in the_Edges_of createGraph(e) by TARSKI:def 1;
    then (the_Source_of createGraph(e)).e0 = (the_Source_of G1).e0 &
      (the_Target_of createGraph(e)).e0 = (the_Target_of G1).e0
      by A5, GLIB_000:def 32;
    hence (the_Source_of G2).e0 = (the_Source_of G1).e0 &
      (the_Target_of G2).e0 = (the_Target_of G1).e0 by A6, GLIB_000:def 32;
  end;
  hence thesis by A2, A3, GLIB_000:def 32;
end;

theorem
  G1 == G2 iff G1.allConnectedSG() = G2.allConnectedSG()
proof
  hereby
    assume G1 == G2;
    then G1 is Subgraph of G2 & G2 is Subgraph of G1 by GLIB_000:87;
    then G2.allConnectedSG() c= G1.allConnectedSG() &
      G1.allConnectedSG() c= G2.allConnectedSG() by Th129;
    hence G1.allConnectedSG() = G2.allConnectedSG() by XBOOLE_0:def 10;
  end;
  assume G1.allConnectedSG() = G2.allConnectedSG();
  then G2 is Subgraph of G1 & G1 is Subgraph of G2 by Th130;
  hence thesis by GLIB_000:87;
end;

theorem Th132:
  for F being PGraphMapping of G1, G2 st F is total
  holds rng(SG2SGFunc(F) | G1.allConnectedSG()) c= G2.allConnectedSG()
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is total;
  set f = SG2SGFunc(F) | G1.allConnectedSG();
  now
    let y be object;
    assume A2: y in rng f;
    then consider x being object such that
      A3: x in dom f & f.x = y by FUNCT_1:def 3;
    reconsider H1 = x as plain connected Subgraph of G1 by A3, Th124;
    y in rng SG2SGFunc(F) by A2, TARSKI:def 3, RELAT_1:70;
    then reconsider H2 = y as plain Subgraph of G2 by Th1;
    A4: H2 = (SG2SGFunc F).x by A3, FUNCT_1:47
      .= rng(F|H1) by Def5;
    now
      let v2,w2 be Vertex of H2;
      A5: F | H1 is total by A1, GLIB_010:57;
      A6: the_Vertices_of H2 = rng(F|H1)_V by A4, A5, GLIB_010:54;
      then consider v1 being object such that
        A7: v1 in dom(F|H1)_V & ((F|H1)_V).v1 = v2 by FUNCT_1:def 3;
      consider w1 being object such that
        A8: w1 in dom(F|H1)_V & ((F|H1)_V).w1 = w2 by A6, FUNCT_1:def 3;
      reconsider v1, w1 as Vertex of H1 by A7, A8;
      consider W1 being Walk of H1 such that
        A9: W1 is_Walk_from v1,w1 by GLIB_002:def 1;
      reconsider F9 = F | H1 as non empty PGraphMapping of H1, rng(F|H1)
        by A5, GLIBPRE1:88;
      F9 is total by A1, GLIBPRE1:109;
      then reconsider W1 as F9-defined Walk of H1 by GLIB_010:121;
      reconsider W2 = F9.:W1 as Walk of H2 by A4;
      take W2;
      F9.:W1 is_Walk_from F9_V.v1, F9_V.w1 by A9, GLIB_010:132;
      hence W2 is_Walk_from v2, w2 by A7, A8, GLIB_001:19;
    end;
    then H2 is connected by GLIB_002:def 1;
    hence y in G2.allConnectedSG() by Th124;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th133:
  for F being PGraphMapping of G1, G2 st F is one-to-one onto
  holds G2.allConnectedSG() c= rng(SG2SGFunc(F) | G1.allConnectedSG())
proof
  let F be PGraphMapping of G1, G2;
  assume A1: F is one-to-one onto;
  set f = SG2SGFunc(F) | G1.allConnectedSG();
  A2: dom f = G1.allConnectedSG() by FUNCT_2:def 1;
  now
    let x be object;
    assume x in G2.allConnectedSG();
    then reconsider H2 = x as plain connected Subgraph of G2 by Th124;
    rng F == G2 by A1, GLIB_010:56;
    then A3: H2 is Subgraph of rng F by GLIB_000:91;
    set H1 = the plain inducedSubgraph of
      G1, F_V"the_Vertices_of H2, F_E"the_Edges_of H2;
    H1 is connected by A1, A3, GLIBPRE1:108;
    then A4: H1 in dom f by A2, Th124;
    A5: rng(F | H1) = H2 by A1, A3, GLIB_009:44, GLIBPRE1:99;
    f.H1 = SG2SGFunc(F).H1 by A4, FUNCT_1:47
      .= H2 by A5, Def5;
    hence x in rng f by A4, FUNCT_1:3;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th134:
  for F being PGraphMapping of G1, G2 st F is isomorphism
  holds G2.allConnectedSG() = rng(SG2SGFunc(F) | G1.allConnectedSG())
proof
  let F be PGraphMapping of G1, G2;
  assume F is isomorphism;
  then rng(SG2SGFunc(F) | G1.allConnectedSG()) c= G2.allConnectedSG() &
    G2.allConnectedSG() c= rng(SG2SGFunc(F) | G1.allConnectedSG())
    by Th132, Th133;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  G2 is G1-Disomorphic implies
    G1.allConnectedSG(),G2.allConnectedSG() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allConnectedSG();
  A2: dom f = G1.allConnectedSG() by FUNCT_2:def 1;
  A3: rng f = G2.allConnectedSG() by A1, Th134;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allConnectedSG();
    then reconsider H = G as plain connected Subgraph of G1 by Th124;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem
  G2 is G1-isomorphic implies
    G1.allConnectedSG(),G2.allConnectedSG() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allConnectedSG();
  A2: dom f = G1.allConnectedSG() by FUNCT_2:def 1;
  A3: rng f = G2.allConnectedSG() by A1, Th134;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allConnectedSG();
    then reconsider H = G as plain connected Subgraph of G1 by Th124;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem
  G is GraphUnion of G.allConnectedSG()
proof
  set G9 = the GraphUnion of G.allConnectedSG();
  G is GraphUnion of G.allSG() by Th35;
  then A1: G9 is Subgraph of G by GLIBPRE1:119;
  now
    A2: for v being Vertex of G holds createGraph(v) in G.allConnectedSG()
      by Th127;
    per cases;
    suppose G is edgeless;
      hence G is Subgraph of G9 by A2, Th24;
    end;
    suppose G is non edgeless;
      then reconsider G0 = G as non edgeless _Graph;
      for e being Edge of G0 holds createGraph(e) in G.allConnectedSG()
        by Th128;
      hence G is Subgraph of G9 by A2, Th25;
    end;
  end;
  hence thesis by A1, GLIB_000:87, GLIB_014:22;
end;

begin :: Tree Subgraph set and Tree Relation

definition
  let G;
  func G.allTrees() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is Tree-like };
  coherence
  proof
    now
      let x be object;
      assume x in { H where H is Element of [#]G.allSG() : H is Tree-like };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is Tree-like;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th138:
  G2 in G1.allTrees() iff G2 is plain Tree-like Subgraph of G1
proof
  hereby
    assume G2 in G1.allTrees();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is Tree-like;
    thus G2 is plain Tree-like Subgraph of G1 by A1;
  end;
  assume A2: G2 is plain Tree-like Subgraph of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th139:
  G.allTrees() = G.allForests() /\ G.allConnectedSG()
proof
  now
    let x be object;
    hereby
      assume x in G.allTrees();
      then x is plain Tree-like Subgraph of G by Th138;
      hence x in G.allForests() & x in G.allConnectedSG() by Th78, Th124;
    end;
    assume x in G.allForests() & x in G.allConnectedSG();
    hence x in G.allTrees() by Th138;
  end;
  hence thesis by XBOOLE_0:def 4;
end;

theorem Th140:
  for H being Tree-like Subgraph of G holds H | _GraphSelectors in G.allTrees()
proof
  let H be Tree-like Subgraph of G;
  H | _GraphSelectors is Tree-like Subgraph of G
    by GLIB_000:92, GLIB_002:48, GLIB_000:128;
  hence thesis by Th138;
end;

theorem Th141:
  G is Tree-like iff G | _GraphSelectors in G.allTrees()
proof
  hereby
    assume A1: G is Tree-like;
    G is Subgraph of G by GLIB_000:40;
    hence G | _GraphSelectors in G.allTrees() by A1, Th140;
  end;
  assume G | _GraphSelectors in G.allTrees();
  then A2: G | _GraphSelectors is Tree-like by Th138;
  G | _GraphSelectors == G by GLIB_000:128;
  hence thesis by A2, GLIB_002:48;
end;

theorem Th142:
  for v being Vertex of G holds createGraph(v) in G.allTrees() by Th138;

theorem Th143:
  for G being non edgeless _Graph, e being Edge of G
  st not e in G.loops() holds createGraph(e) in G.allTrees()
proof
  let G be non edgeless _Graph, e be Edge of G;
  assume not e in G.loops();
  then createGraph(e) is connected acyclic by Th18;
  hence thesis by Th138;
end;

registration
  let G;
  cluster G.allTrees() -> non empty \/-tolerating plain Tree-like simple;
  coherence
  proof
    thus G.allTrees() is non empty by Th142;
    thus G.allTrees() is \/-tolerating plain;
    for H being _Graph st H in G.allTrees() holds H is Tree-like by Th138;
    hence G.allTrees() is Tree-like by GLIB_014:def 10;
    hence thesis;
  end;
end;

theorem Th144:
  H.allTrees() c= G.allTrees()
proof
  now
    let x be object;
    assume x in H.allTrees();
    then reconsider H9 = x as plain Tree-like Subgraph of H by Th138;
    H9 is Subgraph of G by GLIB_000:43;
    hence x in G.allTrees() by Th138;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th145:
  for G2 being loopless _Graph st G2.allTrees() c= G1.allTrees()
  holds G2 is Subgraph of G1
proof
  let G2 be loopless _Graph;
  assume A1: G2.allTrees() c= G1.allTrees();
  now
    let x be object;
    assume x in the_Vertices_of G2;
    then reconsider v = x as Vertex of G2;
    set H = createGraph(v);
    H in G2.allTrees() by Th142;
    then H is Subgraph of G1 by A1, Th138;
    then the_Vertices_of H c= the_Vertices_of G1 by GLIB_000:def 32;
    hence x in the_Vertices_of G1 by ZFMISC_1:31;
  end;
  then A2: the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
  now
    let x be object;
    assume A3: x in the_Edges_of G2;
    then reconsider G9 = G2 as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A3;
    set H = createGraph(e);
    not e in G9.loops();
    then H in G2.allTrees() by Th143;
    then H is Subgraph of G1 by A1, Th138;
    then the_Edges_of H c= the_Edges_of G1 by GLIB_000:def 32;
    then {e} c= the_Edges_of G1 by Th13;
    hence x in the_Edges_of G1 by ZFMISC_1:31;
  end;
  then A4: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
  now
    let x be set;
    assume A5: x in the_Edges_of G2;
    then reconsider G9 = G2 as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A5;
    set H = createGraph(e);
    not e in G9.loops();
    then H in G2.allTrees() by Th143;
    then A6: H is Subgraph of G1 & H is Subgraph of G2 by A1, Th138;
    the_Edges_of H = {e} by Th13;
    then A7: x in the_Edges_of H by TARSKI:def 1;
    thus (the_Source_of G2).x = (the_Source_of H).x by A7, GLIB_000:def 32
      .= (the_Source_of G1).x by A6, A7, GLIB_000:def 32;
    thus (the_Target_of G2).x = (the_Target_of H).x by A7, GLIB_000:def 32
      .= (the_Target_of G1).x by A6, A7, GLIB_000:def 32;
  end;
  hence thesis by A2, A4, GLIB_000:def 32;
end;

theorem Th146:
  for H being removeLoops of G holds G.allTrees() = H.allTrees()
proof
  let H be removeLoops of G;
  A1: H.allTrees() c= G.allTrees() by Th144;
  now
    let z be object;
    assume z in G.allTrees();
    then reconsider H9 = z as plain Tree-like Subgraph of G by Th138;
    the_Vertices_of H9 c= the_Vertices_of G;
    then A2: the_Vertices_of H9 c= the_Vertices_of H by GLIB_000:def 33;
    now
      let x be object;
      assume A3: x in the_Edges_of H9;
      then A4: x in the_Edges_of G;
      not x in G.loops()
      proof
        assume x in G.loops();
        then consider v being object such that
          A5: x Joins v,v,G by GLIB_009:def 2;
        x is set & v is set by TARSKI:1;
        then x Joins v,v,H9 by A3, A5, GLIB_000:73;
        then x in H9.loops() by GLIB_009:def 2;
        hence contradiction;
      end;
      then x in the_Edges_of G \ G.loops() by A4, XBOOLE_0:def 5;
      hence x in the_Edges_of H by GLIB_000:53;
    end;
    then the_Edges_of H9 c= the_Edges_of H by TARSKI:def 3;
    then H9 is Subgraph of H by A2, GLIB_000:44;
    hence z in H.allTrees() by Th138;
  end;
  then G.allTrees() c= H.allTrees() by TARSKI:def 3;
  hence thesis by A1, XBOOLE_0:def 10;
end;

theorem Th147:
  for G1, G2 being loopless _Graph
  holds G1 == G2 iff G1.allTrees() = G2.allTrees()
proof
  let G1, G2 be loopless _Graph;
  hereby
    assume G1 == G2;
    then G2 is removeLoops of G1 by GLIB_009:58;
    hence G1.allTrees() = G2.allTrees() by Th146;
  end;
  assume G1.allTrees() = G2.allTrees();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th145;
  hence thesis by GLIB_000:87;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G3 == G4 iff G1.allTrees() = G2.allTrees()
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  hereby
    assume A1: G3 == G4;
    thus G1.allTrees() = G3.allTrees() by Th146
      .= G4.allTrees() by A1, Th147
      .= G2.allTrees() by Th146;
  end;
  assume A2: G1.allTrees() = G2.allTrees();
  G3.allTrees() = G1.allTrees() by Th146
    .= G4.allTrees() by A2, Th146;
  hence thesis by Th147;
end;

theorem Th149:
  for F being PGraphMapping of G1, G2 st F is weak_SG-embedding
  holds rng(SG2SGFunc(F) | G1.allTrees()) c= G2.allTrees()
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  f | G1.allTrees() = f | (G1.allConnectedSG() /\ G1.allForests()) by Th139
    .= (f | G1.allConnectedSG()) /\ (f | G1.allForests()) by RELAT_1:79;
  then A1: rng(f | G1.allTrees()) c=
    rng(f|G1.allConnectedSG()) /\ rng(f|G1.allForests()) by RELAT_1:13;
  assume F is weak_SG-embedding;
  then rng(f | G1.allConnectedSG()) c= G2.allConnectedSG() &
    rng(f | G1.allForests()) c= G2.allForests() by Th90, Th132;
  then rng(f | G1.allConnectedSG()) /\ rng(f | G1.allForests())
    c= G2.allConnectedSG() /\ G2.allForests() by XBOOLE_1:27;
  then rng(f|G1.allConnectedSG()) /\ rng(f|G1.allForests()) c= G2.allTrees()
    by Th139;
  hence thesis by A1, XBOOLE_1:1;
end;

theorem Th150:
  for F being PGraphMapping of G1, G2 st F is weak_SG-embedding onto
  holds G2.allTrees() = rng(SG2SGFunc(F) | G1.allTrees())
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  assume A1: F is weak_SG-embedding onto;
  then G2.allForests() c= rng(f | G1.allForests()) &
    G2.allConnectedSG() c= rng(f | G1.allConnectedSG()) by Th91, Th133;
  then G2.allForests() /\ G2.allConnectedSG() c=
    rng(f | G1.allForests()) /\ rng(f | G1.allConnectedSG())
    by XBOOLE_1:27;
  then A2: G2.allTrees() c=
    rng(f | G1.allForests()) /\ rng(f | G1.allConnectedSG()) by Th139;
  A3: rng(SG2SGFunc(F) | G1.allTrees()) c= G2.allTrees() by A1, Th149;
  A4: rng(f | G1.allForests()) = f.:G1.allForests() by RELAT_1:115;
  A5: rng(f | G1.allConnectedSG()) = f.:G1.allConnectedSG()
    by RELAT_1:115;
  A6: f is one-to-one by A1, Th31;
  rng(f | G1.allForests()) /\ rng(f | G1.allConnectedSG())
     = f.:(G1.allForests() /\ G1.allConnectedSG()) by A4, A5, A6, FUNCT_1:62
    .= rng(f | (G1.allForests() /\ G1.allConnectedSG())) by RELAT_1:115
    .= rng(f | G1.allTrees()) by Th139;
  hence thesis by A3, A2, XBOOLE_0:def 10;
end;

theorem Th151:
  for G1, G2 being _Graph holds G2 is G1-Disomorphic implies
    G1.allTrees(),G2.allTrees() are_Disomorphic
proof
  let G1, G2 be _Graph;
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allTrees();
  A2: dom f = G1.allTrees() by FUNCT_2:def 1;
  A3: rng f = G2.allTrees() by A1, Th150;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allTrees();
    then reconsider H = G as plain Tree-like Subgraph of G1 by Th138;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem Th152:
  for G1, G2 being _Graph holds G2 is G1-isomorphic implies
    G1.allTrees(),G2.allTrees() are_isomorphic
proof
  let G1, G2 be _Graph;
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allTrees();
  A2: dom f = G1.allTrees() by FUNCT_2:def 1;
  A3: rng f = G2.allTrees() by A1, Th150;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allTrees();
    then reconsider H = G as plain Tree-like Subgraph of G1 by Th138;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-Disomorphic implies
    G1.allTrees(),G2.allTrees() are_Disomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allTrees() = G3.allTrees() & G2.allTrees() = G4.allTrees() by Th146;
  hence thesis by Th151;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-isomorphic implies
    G1.allTrees(),G2.allTrees() are_isomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allTrees() = G3.allTrees() & G2.allTrees() = G4.allTrees() by Th146;
  hence thesis by Th152;
end;

theorem Th155:
  for H being removeLoops of G holds H is GraphUnion of G.allTrees()
proof
  let H be removeLoops of G;
  set G9 = the GraphUnion of G.allTrees();
  reconsider G8 = G as GraphUnion of G.allSG() by Th35;
  set H9 = the GraphUnion of {H};
  now
    thus G9 is Subgraph of G8 by GLIBPRE1:119;
    now
      let x be object;
      assume x in the_Vertices_of H;
      then reconsider v = x as Vertex of G;
      set H8 = createGraph(v);
      H8 in G.allTrees() by Th142;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Vertices_of H8 c= the_Vertices_of G9 by GLIB_000:def 32;
      hence x in the_Vertices_of G9 by ZFMISC_1:31;
    end;
    hence the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;
    now
      let x be object;
      assume x in the_Edges_of H;
      then x in the_Edges_of G \ G.loops() by GLIB_000:53;
      then A1: x in the_Edges_of G & not x in G.loops() by XBOOLE_0:def 5;
      then reconsider G0 = G as non edgeless _Graph;
      reconsider e = x as Edge of G0 by A1;
      set H8 = createGraph(e);
      H8 in G.allTrees() by A1, Th143;
      then H8 is Subgraph of G9 by GLIB_014:21;
      then the_Edges_of H8 c= the_Edges_of G9 by GLIB_000:def 32;
      then {e} c= the_Edges_of G9 by Th13;
      hence x in the_Edges_of G9 by ZFMISC_1:31;
    end;
    hence the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;
  end;
  then A2: H is Subgraph of G9 by GLIB_000:44;
  now
    let H2 be Element of G.allTrees();
    reconsider H1 = H as Element of {H} by TARSKI:def 1;
    take H1;
    H.allTrees() = G.allTrees() by Th146;
    hence H2 is Subgraph of H1 by Th138;
  end;
  then G9 is Subgraph of H9 by GLIBPRE1:118;
  then G9 is Subgraph of H by GLIB_000:91, GLIB_014:24;
  hence thesis by A2, GLIB_000:87, GLIB_014:22;
end;

theorem
  G is loopless iff G is GraphUnion of G.allTrees()
proof
  hereby
    set H = the removeLoops of G;
    assume G is loopless;
    then A1: G == H by GLIB_009:58;
    H is GraphUnion of G.allTrees() by Th155;
    hence G is GraphUnion of G.allTrees() by A1, GLIB_014:22;
  end;
  assume G is GraphUnion of G.allTrees();
  hence G is loopless;
end;

theorem Th157:
  the_Edges_of G = G.loops() iff G.allTrees() is edgeless
proof
  hereby
    set H = the removeLoops of G;
    assume A1: the_Edges_of G = G.loops();
    now
      let H be _Graph;
      assume H in G.allTrees();
      then A2: H is Tree-like Subgraph of G by Th138;
      now
        assume the_Edges_of H <> {};
        then consider e being object such that
          A3: e in the_Edges_of H by XBOOLE_0:def 1;
        the_Edges_of H c= the_Edges_of G by A2, GLIB_000:def 32;
        then consider v being object such that
          A4: e Joins v,v,G by A1, A3, GLIB_009:def 2;
        e is set & v is set by TARSKI:1;
        then e Joins v,v,H by A2, A3, A4, GLIB_000:73;
        hence contradiction by A2, GLIB_000:18;
      end;
      hence H is edgeless;
    end;
    hence G.allTrees() is edgeless by GLIB_014:def 12;
  end;
  assume A5: G.allTrees() is edgeless;
  now
    let x be object;
    assume A6: x in the_Edges_of G;
    then reconsider G9 = G as non edgeless _Graph;
    reconsider e = x as Edge of G9 by A6;
    set H9 = createGraph(e);
    assume not x in G.loops();
    then H9 in G.allTrees() by Th143;
    hence contradiction by A5;
  end;
  then the_Edges_of G c= G.loops() by TARSKI:def 3;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  the_Edges_of G = G.loops() iff
    G.allTrees() = the set of all createGraph(v) where v is Vertex of G
proof
  set S = the set of all createGraph(v) where v is Vertex of G;
  hereby
    assume the_Edges_of G = G.loops();
    then A1: G.allTrees() is edgeless by Th157;
    now
      let x be object;
      hereby
        assume A2: x in G.allTrees();
        then reconsider H = x as plain Tree-like Subgraph of G by Th138;
        reconsider V = the_Vertices_of H as non empty Subset of
          the_Vertices_of G;
        set H9 = createGraph(V);
        reconsider H9 as plain Subgraph of G;
        A3: the_Vertices_of H = the_Vertices_of H9;
        A4: the_Edges_of H = {} by A1, A2;
        then the_Edges_of H = the_Edges_of H9;
        then H is Subgraph of H9 & H9 is Subgraph of H by A3, GLIB_000:44;
        then A5: H = H9 by GLIB_000:87, GLIB_009:44;
        H is edgeless by A4;
        then consider v being Vertex of H such that
          A6: the_Vertices_of H = {v} by GLIB_000:22;
        the_Vertices_of H c= the_Vertices_of G;
        then reconsider v as Vertex of G by TARSKI:def 3;
        H9 = createGraph(v) by A6;
        hence x in S by A5;
      end;
      assume x in S;
      then consider v being Vertex of G such that
        A7: x = createGraph(v);
      thus x in G.allTrees() by A7, Th142;
    end;
    hence G.allTrees() = S by TARSKI:2;
  end;
  assume A8: G.allTrees() = S;
  now
    let H be _Graph;
    assume H in G.allTrees();
    then consider v being Vertex of G such that
      A9: H = createGraph(v) by A8;
    thus H is edgeless by A9;
  end;
  then G.allTrees() is edgeless by GLIB_014:def 12;
  hence thesis by Th157;
end;

definition
  let G;
  func SubtreeRel(G) -> Relation of G.allTrees() equals
  (SubgraphRel G) |_2 G.allTrees();
  coherence;
end;

theorem Th159:
  for H1, H2 being plain Tree-like Subgraph of G
  holds [H1,H2] in SubtreeRel(G) iff H1 is Subgraph of H2
proof
  let H1, H2 be plain Tree-like Subgraph of G;
  A1: H1 in G.allSG() & H2 in G.allSG() by Th1;
  hereby
    assume [H1,H2] in SubtreeRel(G);
    then [H1,H2] in SubgraphRel(G) by MMLQUER2:4;
    hence H1 is Subgraph of H2 by A1, Def6;
  end;
  A2: H1 in G.allTrees() & H2 in G.allTrees() by Th138;
  assume H1 is Subgraph of H2;
  then [H1,H2] in SubgraphRel(G) by A1, Def6;
  hence thesis by A2, MMLQUER2:4;
end;

theorem Th160:
  field SubtreeRel(G) = G.allTrees()
proof
  G.allTrees() c= G.allSG();
  then G.allTrees() c= field SubgraphRel(G) by Th40;
  hence thesis by ORDERS_1:71;
end;

theorem Th161:
  SubtreeRel(G) partially_orders G.allTrees()
proof
  SubgraphRel(G) partially_orders G.allTrees() by Th41, ORDERS_1:35;
  then SubtreeRel(G) is being_partial-order by ORDERS_1:36;
  then SubtreeRel(G) partially_orders field SubtreeRel(G) by ORDERS_1:34;
  hence thesis by Th160;
end;

registration
  let G;
  cluster SubtreeRel(G) -> reflexive antisymmetric transitive
    being_partial-order;
  coherence
  proof
    A1: SubtreeRel(G) partially_orders G.allTrees() by Th161;
    A2: G.allTrees() = field SubtreeRel(G) by Th160;
    thus A3: SubtreeRel(G) is reflexive
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 9;
    thus A4: SubtreeRel(G) is antisymmetric
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 12;
    thus SubtreeRel(G) is transitive
      by A1, A2, ORDERS_1:def 8, RELAT_2:def 16;
    hence thesis by A3, A4, ORDERS_1:def 5;
  end;
end;

theorem Th162:
  SubtreeRel(H) = (SubtreeRel G) |_2 H.allTrees()
proof
  thus SubtreeRel(H) = ((SubgraphRel G) |_2 H.allSG()) |_2 H.allTrees() by Th43
    .= (SubgraphRel G) |_2 (H.allSG() /\ H.allTrees()) by WELLORD1:19
    .= (SubgraphRel G) |_2 (H.allTrees()) by XBOOLE_1:28
    .= (SubgraphRel G) |_2 (G.allTrees() /\ H.allTrees()) by Th144, XBOOLE_1:28
    .= (SubtreeRel G) |_2 H.allTrees() by WELLORD1:19;
end;

theorem Th163:
  for G being loopless _Graph
  holds G is edgeless iff SubtreeRel(G) = id G.allTrees()
proof
  let G be loopless _Graph;
  hereby
    assume A1: G is edgeless;
    now
      let x,y be object;
      hereby
        assume A2: [x,y] in SubtreeRel(G);
        then x in field SubtreeRel(G) by RELAT_1:15;
        hence x in G.allTrees() by Th160;
        then reconsider T1 = x as plain Tree-like Subgraph of G by Th138;
        y in field SubtreeRel(G) by A2, RELAT_1:15;
        then y in G.allTrees() by Th160;
        then reconsider T2 = y as plain Tree-like Subgraph of G by Th138;
        A3: T2 is edgeless by A1;
        then consider v being Vertex of T2 such that
          A4: the_Vertices_of T2 = {v} by GLIB_000:22;
        A5: T1 is Subgraph of T2 by A2, Th159;
        then the_Vertices_of T1 c= the_Vertices_of T2 by GLIB_000:def 32;
        then A6: the_Vertices_of T2 c= the_Vertices_of T1 by A4, ZFMISC_1:33;
        the_Edges_of T2 = {} by A3;
        then the_Edges_of T2 c= the_Edges_of T1 by XBOOLE_1:2;
        then T2 is Subgraph of T1 by A6, GLIB_000:44;
        hence x = y by A5, GLIB_000:87, GLIB_009:44;
      end;
      assume A7: x in G.allTrees() & x = y;
      SubtreeRel(G) is_reflexive_in field SubtreeRel(G) by RELAT_2:def 9;
      then SubtreeRel(G) is_reflexive_in G.allTrees() by Th160;
      hence [x,y] in SubtreeRel(G) by A7, RELAT_2:def 1;
    end;
    hence SubtreeRel(G) = id G.allTrees() by RELAT_1:def 10;
  end;
  assume A8: SubtreeRel(G) = id G.allTrees();
  assume G is non edgeless;
  then reconsider G9 = G as non edgeless _Graph;
  set e = the Edge of G9;
  set v = (the_Source_of G9).e, w = (the_Target_of G9).e, V = {v,w};
  A9: e Joins v,w,G9 by GLIB_000:def 13;
  reconsider V as non empty Subset of the_Vertices_of G9;
  set S = e .--> v, T = e .--> w;
  dom S = dom{[e,v]} & dom T = dom{[e,w]} by FUNCT_4:82;
  then A10: dom S = {e} & dom T = {e} by RELAT_1:9;
  rng S = {v} & rng T = {w} by FUNCOP_1:88;
  then reconsider S, T as Function of {e}, V by A10, FUNCT_2:2, ZFMISC_1:7;
  set H9 = createGraph(e);
  not e in G9.loops();
  then A11: H9 in G.allTrees() by Th143;
  set H8 = the plain inducedSubgraph of H9, {v};
  the_Edges_of H9 = {e} by Th13;
  then A12: e in the_Edges_of H9 by TARSKI:def 1;
  e Joins v,w,H9 by A12, A9, GLIB_000:73;
  then A14: v is Vertex of H9 by GLIB_000:13;
  A15: H8 is Subgraph of G by GLIB_000:43;
  H8 is loopless _trivial by A14;
  then A16: H8 is _trivial edgeless;
  then A17: H8 is plain Tree-like Subgraph of G by A15;
  A18: H8 <> H9 by A16;
  [H8, H9] in SubtreeRel(G) by A11, A17, Th159;
  hence contradiction by A18, A8, RELAT_1:def 10;
end;

theorem Th164:
  for H being removeLoops of G holds SubtreeRel(G) = SubtreeRel(H)
proof
  let H be removeLoops of G;
  thus SubtreeRel(G) = (SubtreeRel G) |_2 G.allTrees() by WELLORD1:21
    .= (SubtreeRel G) |_2 H.allTrees() by Th146
    .= SubtreeRel(H) by Th162;
end;

theorem
  the_Edges_of G = G.loops() iff SubtreeRel(G) = id G.allTrees()
proof
  set H = the removeLoops of G;
  hereby
    assume the_Edges_of G = G.loops();
    then A1: H is edgeless;
    thus SubtreeRel(G) = SubtreeRel(H) by Th164
      .= id H.allTrees() by A1, Th163
      .= id G.allTrees() by Th146;
  end;
  assume A2: SubtreeRel(G) = id G.allTrees();
  SubtreeRel(H) = SubtreeRel(G) by Th164
    .= id H.allTrees() by A2, Th146;
  then H is edgeless by Th163;
  hence thesis by GLIBPRE1:70;
end;

theorem Th166:
  G.allTrees() has_upper_Zorn_property_wrt SubtreeRel(G)
proof
  now
    let Y be set;
    assume that
      A1: Y c= G.allTrees() and
      A2: (SubtreeRel G) |_2 Y is being_linear-order;
    per cases;
    suppose A3: Y <> {};
      A4: Y c= G.allSG() by A1, XBOOLE_1:1;
      then reconsider S = Y as GraphUnionSet by A3;
      set T = the plain GraphUnion of S;
      now
        let v1,v2 be Vertex of T;
        A5: the_Vertices_of T = union the_Vertices_of S by GLIB_014:def 25;
        then consider V1 being set such that
          A6: v1 in V1 & V1 in the_Vertices_of S by TARSKI:def 4;
        consider H1 being _Graph such that
          A7: H1 in S & V1 = the_Vertices_of H1 by A6, GLIB_014:def 14;
        consider V2 being set such that
          A8: v2 in V2 & V2 in the_Vertices_of S by A5, TARSKI:def 4;
        consider H2 being _Graph such that
          A9: H2 in S & V2 = the_Vertices_of H2 by A8, GLIB_014:def 14;
        reconsider H1, H2 as Element of G.allTrees() by A1, A7, A9;
        Y c= field SubtreeRel(G) by A1, Th160;
        then A10: field((SubtreeRel G)|_2 Y) = Y by ORDERS_1:71;
        (SubtreeRel G) |_2 Y is reflexive connected by A2, ORDERS_1:def 6;
        then per cases by A7, A9, A10, RELAT_2:def 7, RELAT_2:def 15;
        suppose [H1,H2] in (SubtreeRel G) |_2 Y;
          then [H1,H2] in SubtreeRel(G) by MMLQUER2:4;
          then H1 is Subgraph of H2 by Th159;
          then the_Vertices_of H1 c= the_Vertices_of H2 by GLIB_000:def 32;
          then consider W2 being Walk of H2 such that
            A11: W2 is_Walk_from v1,v2 by A6, A7, A8, A9, GLIB_002:def 1;
          H2 is Subgraph of T by A9, GLIB_014:21;
          then reconsider W = W2 as Walk of T by GLIB_001:167;
          take W;
          thus W is_Walk_from v1,v2 by A11, GLIB_001:19;
        end;
        suppose [H2,H1] in (SubtreeRel G) |_2 Y;
          then [H2,H1] in SubtreeRel(G) by MMLQUER2:4;
          then H2 is Subgraph of H1 by Th159;
          then the_Vertices_of H2 c= the_Vertices_of H1 by GLIB_000:def 32;
          then consider W1 being Walk of H1 such that
            A12: W1 is_Walk_from v1,v2 by A6, A7, A8, A9, GLIB_002:def 1;
          H1 is Subgraph of T by A7, GLIB_014:21;
          then reconsider W = W1 as Walk of T by GLIB_001:167;
          take W;
          thus W is_Walk_from v1,v2 by A12, GLIB_001:19;
        end;
      end;
      then reconsider T as connected _Graph by GLIB_002:def 1;
      now
        given W being Walk of T such that
          A13: W is Cycle-like;
        (SubtreeRel G) |_2 Y = (SubgraphRel G) |_2 S by A1, WELLORD1:22;
        then consider H being Element of S such that
          A14: W is Walk of H by A2, A4, Th44;
        reconsider W as Walk of H by A14;
        W is Cycle-like by A13, GLIB_006:24;
        hence contradiction by A1, GLIB_002:def 2;
      end;
      then T is acyclic by GLIB_002:def 2;
      then reconsider T as Tree-like _Graph;
      A15: S c= G.allSG() by A1, XBOOLE_1:1;
      G is GraphUnion of G.allSG() by Th35;
      then reconsider T as Tree-like Subgraph of G by A15, GLIBPRE1:119;
      reconsider x = T as set;
      take x;
      thus x in G.allTrees() by Th138;
      let y be set;
      assume A16: y in Y;
      then reconsider T9 = y as Element of G.allTrees() by A1;
      T9 is Subgraph of T by A16, GLIB_014:21;
      hence [y,x] in SubtreeRel(G) by Th159;
    end;
    suppose A17: Y = {};
      reconsider x = the Element of G.allTrees() as set;
      take x;
      thus x in G.allTrees();
      thus for y being set st y in Y holds [y,x] in SubtreeRel(G) by A17;
    end;
  end;
  hence thesis by ORDERS_1:def 10;
end;

registration
  let G be connected _Graph;
  ::$N every connected graph has a spanning tree
  cluster plain spanning Tree-like for Subgraph of G;
  existence
  proof
    A1: field SubtreeRel(G) = G.allTrees() by Th160;
    SubtreeRel(G) partially_orders G.allTrees() by Th161;
    then consider x being set such that
      A2: x is_maximal_in SubtreeRel(G) by A1, Th166, ORDERS_1:63;
    x in field SubtreeRel(G) by A2, ORDERS_1:def 12;
    then reconsider T = x as plain Tree-like Subgraph of G by A1, Th138;
    take T;
    per cases;
    suppose G is _trivial;
      hence thesis by GLIB_000:121;
    end;
    suppose A3: G is non _trivial;
      now
        assume T is non spanning;
        then consider v,e,w being object such that
          A4: v <> w & e DJoins v,w,G & not e in the_Edges_of T and
          A5: for G3 being addAdjVertex of T,v,e,w holds G3 is Subgraph of G
          and A6: (v in the_Vertices_of T & not w in the_Vertices_of T) or
            (not v in the_Vertices_of T & w in the_Vertices_of T)
          by A3, GLIBPRE1:61;
        set G3 = the plain addAdjVertex of T,v,e,w;
        reconsider G3 as plain Tree-like Subgraph of G by A5;
        e DJoins v,w,G3 by A4, A6, GLIB_006:131, GLIB_006:132;
        then A7: T <> G3 by A4, GLIB_000:def 14;
        A8: G3 in field SubtreeRel(G) by A1, Th138;
        T is Subgraph of G3 by GLIB_006:57;
        then [T,G3] in SubtreeRel(G) by Th159;
        hence contradiction by A2, A7, A8, ORDERS_1:def 12;
      end;
      hence thesis;
    end;
  end;
end;

theorem Th167:
  for G being connected _Graph, e being object
  st e in the_Edges_of G \ G.loops()
  ex T being plain spanning Tree-like Subgraph of G
  st e in the_Edges_of T
proof
  let G be connected _Graph, e be object;
  assume e in the_Edges_of G \ G.loops();
  then A1: e in the_Edges_of G & not e in G.loops() by XBOOLE_0:def 5;
  set T1 = the plain spanning Tree-like Subgraph of G;
  per cases;
  suppose A2: e in the_Edges_of T1; :: trivial case
    take T1;
    thus thesis by A2;
  end;
  suppose A3: not e in the_Edges_of T1;
    :: the idea is to add the specified edge but remove another
    :: edge from the cycle that will be formed, so that the
    :: resulting graph T3 is a spanning tree containing the specified edge
    set v = (the_Source_of G).e, w = (the_Target_of G).e;
    set G2 = the addEdge of T1,v,e,w;
    e DJoins v,w,G by A1, GLIB_000:def 14;
    then reconsider G2 as Subgraph of G by GLIBPRE1:50;
    :: show that G2 contains only one cycle
    v is Vertex of G & w is Vertex of G by A1, FUNCT_2:5;
    then A4: v is Vertex of T1 & w is Vertex of T1 by GLIB_000:def 33;
    then A5: G2 is non acyclic & for W1, W2 being Walk of G2
        st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges()
      by A3, GLIBPRE1:51;
    then consider W being Walk of G2 such that
      A6: W is Cycle-like by GLIB_002:def 2;
    :: show that the cycle contains another edge e0
    A7: e in W.edges()
    proof
      assume not e in W.edges();
      then reconsider W1 = W as Walk of T1 by A4, GLIB_006:109;
      W1 is Cycle-like by A6, GLIB_006:24;
      hence contradiction by GLIB_002:def 2;
    end;
    G2.loops() c= G.loops() by GLIB_009:48;
    then not e in G2.loops() by A1;
    then consider e0 being object such that
      A8: e0 in W.edges() & e0 <> e by A6, A7, GLIBPRE1:29;
    reconsider e0 as set by TARSKI:1;
    :: T3 is the desired spanning tree
    set T3 = the plain removeEdge of G2,e0;
    set w1 = (the_Source_of G2).e0, w2 = (the_Target_of G2).e0;
    A9: G2 is addEdge of T3,w1,e0,w2 by A8, GLIB_008:37;
    A10: e0 Joins w1,w2,G2 by A8, GLIB_000:def 13;
    e0 in {e0} by TARSKI:def 1;
    then not e0 in the_Edges_of G2 \ {e0} by XBOOLE_0:def 5;
    then A11: not e0 in the_Edges_of T3 by GLIB_000:51;
    w1 in the_Vertices_of G2 & w2 in the_Vertices_of G2 by A10, GLIB_000:13;
    then A12: w1 is Vertex of T3 & w2 is Vertex of T3 by GLIB_000:def 33;
    :: show that T3 is connected
    now
      let v1, v2 be Vertex of T3;
      reconsider u1 = v1, u2 = v2 as Vertex of G2 by GLIB_000:def 33;
      consider W2 being Walk of G2 such that
        A13: W2 is_Walk_from u1,u2 by GLIB_002:def 1;
      set P2 = the Path-like Subwalk of W2;
      A14: P2 is_Walk_from u1,u2 by A13, GLIB_001:160;
      per cases;
      suppose not e0 in P2.edges(); :: trivial case
        then reconsider W3 = P2 as Walk of T3 by GLIB_001:172;
        take W3;
        thus W3 is_Walk_from v1,v2 by A14, GLIB_001:19;
      end;
      suppose A15: e0 in P2.edges();
        :: from the cycle in G2 we can get a path avoiding e0
        consider P4 being Path of G2 such that
          A16: P4 is_Walk_from w1,w2 & P4.edges() = W.edges()\{e0} and
          not e0 in G2.loops() implies P4 is open by A6, A8, A10, GLIBPRE1:32;
        e0 in {e0} by TARSKI:def 1;
        then A17: not e0 in P4.edges() by A16, XBOOLE_0:def 5;
        A18: P4.first() = w1 & P4.last() = w2 by A16, GLIB_001:def 23;
        :: replace e0 in P2 by the avoiding path
        :: the distinction of cases comes from the orientation of e0 in P2
        per cases by A10, A15, GLIB_006:28;
        suppose A19: G2.walkOf(w1,e0,w2) is_odd_substring_of P2, 0;
          set W4 = P2.replaceEdgeWith(e0,P4);
          e0 Joins P4.first(),P4.last(),G2 &
            G2.walkOf(P4.first(),e0,P4.last()) is_odd_substring_of P2, 0
            by A10, A18, A19;
          then not e0 in W4.edges() by A17, GLIB_006:40;
          then reconsider W3 = W4 as Walk of T3 by GLIB_001:172;
          take W3;
          W4 is_Walk_from u1,u2 by A14, GLIB_006:47;
          hence W3 is_Walk_from v1,v2 by GLIB_001:19;
        end;
        suppose A20: G2.walkOf(w2,e0,w1) is_odd_substring_of P2, 0;
          set W4 = P2.replaceEdgeWith(e0,P4.reverse());
          A21: not e0 in P4.reverse().edges() by A17, GLIB_001:107;
          P4.reverse().first() = w2 & P4.reverse().last() = w1
            by A18, GLIB_001:22;
          then e0 Joins P4.reverse().first(),P4.reverse().last(),G2 &
            G2.walkOf(P4.reverse().first(),e0,P4.reverse().last())
              is_odd_substring_of P2, 0 by A10, A20, GLIB_000:14;
          then not e0 in W4.edges() by A21, GLIB_006:40;
          then reconsider W3 = W4 as Walk of T3 by GLIB_001:172;
          take W3;
          W4 is_Walk_from u1,u2 by A14, GLIB_006:47;
          hence W3 is_Walk_from v1,v2 by GLIB_001:19;
        end;
      end;
    end;
    then T3 is connected by GLIB_002:def 1;
    :: since G2 only contains one cycle and T3 is connected, it is a tree
    then A22: T3 is Tree-like by A5, A9, A11, A12, GLIBPRE1:52;
    the_Vertices_of T3 = the_Vertices_of G2 by GLIB_000:def 33
      .= the_Vertices_of T1 by A4, GLIB_006:102
      .= the_Vertices_of G by GLIB_000:def 33;
    then reconsider T3 as plain Tree-like spanning Subgraph of G
      by A22, GLIB_000:def 33, GLIB_000:43;
    take T3;
    not e in {e0} by A8, TARSKI:def 1;
    then e in the_Edges_of G2 \ {e0} by A7, XBOOLE_0:def 5;
    hence e in the_Edges_of T3 by GLIB_000:51;
  end;
end;

begin :: Spanning Tree Subgraph set

definition
  let G;
  func G.allSpanningTrees() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is spanning Tree-like };
  coherence
  proof
    now
      let x be object;
      assume x in { H
        where H is Element of [#]G.allSG() : H is spanning Tree-like };
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is spanning Tree-like;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th168:
  G2 in G1.allSpanningTrees() iff
    G2 is plain spanning acyclic Subgraph of G1 & G2 is connected
proof
  hereby
    assume G2 in G1.allSpanningTrees();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is spanning Tree-like;
    thus G2 is plain spanning acyclic Subgraph of G1 by A1;
    thus G2 is connected by A1;
  end;
  assume A2: G2 is plain spanning acyclic Subgraph of G1 & G2 is connected;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem Th169:
  G.allSpanningTrees() = G.allSpanningSG() /\ G.allTrees()
proof
  now
    let x be object;
    hereby
      assume A1: x in G.allSpanningTrees();
      then reconsider H = x as plain spanning acyclic Subgraph of G by Th168;
      H is connected by A1, Th168;
      hence x in G.allSpanningSG() & x in G.allTrees() by Th60, Th138;
    end;
    assume A2: x in G.allSpanningSG() & x in G.allTrees();
    then reconsider H = x as plain spanning acyclic Subgraph of G by Th60;
    H is connected by A2;
    hence x in G.allSpanningTrees() by Th168;
  end;
  hence thesis by XBOOLE_0:def 4;
end;

theorem Th170:
  G.allSpanningTrees() = G.allConnectedSG() /\ G.allSpanningForests()
proof
  now
    let x be object;
    hereby
      assume x in G.allSpanningTrees();
      then x is plain spanning acyclic Subgraph of G & x is connected _Graph
        by Th168;
      hence x in G.allConnectedSG() & x in G.allSpanningForests() by Th102,
Th124;
    end;
    assume x in G.allConnectedSG() & x in G.allSpanningForests();
    then x is plain spanning Subgraph of G & x is plain Tree-like Subgraph of G
      by Th102;
    hence x in G.allSpanningTrees() by Th168;
  end;
  hence thesis by XBOOLE_0:def 4;
end;

theorem
  for H being spanning acyclic Subgraph of G st H is connected
  holds H | _GraphSelectors in G.allSpanningTrees()
proof
  let H be spanning acyclic Subgraph of G;
  assume A1: H is connected;
  A2: H | _GraphSelectors == H by GLIB_000:128;
  then H | _GraphSelectors is spanning acyclic Subgraph of G
    by GLIB_000:171, GLIB_002:44;
  hence thesis by A1, A2, Th168, GLIB_002:8;
end;

theorem Th172:
  G is Tree-like iff G | _GraphSelectors in G.allSpanningTrees()
proof
  A1: G.allSpanningTrees() = G.allSpanningSG() /\ G.allTrees() by Th169;
  hereby
    assume G is Tree-like;
    then A2: G | _GraphSelectors in G.allTrees() by Th141;
    G | _GraphSelectors in G.allSpanningSG() by Th62;
    hence G | _GraphSelectors in G.allSpanningTrees()
      by A1, A2, XBOOLE_0:def 4;
  end;
  assume G | _GraphSelectors in G.allSpanningTrees();
  then G | _GraphSelectors in G.allTrees() by A1;
  hence G is Tree-like by Th141;
end;

theorem Th173:
  G is connected iff G.allSpanningTrees() <> {}
proof
  hereby
    assume G is connected;
    then reconsider G0 = G as connected _Graph;
    the plain spanning Tree-like Subgraph of G0 in G.allSpanningTrees()
      by Th168;
    hence G.allSpanningTrees() <> {};
  end;
  assume A1: G.allSpanningTrees() <> {};
  set x = the Element of G.allSpanningTrees();
  reconsider H = x as plain spanning acyclic Subgraph of G by A1, Th168;
  H is connected by A1, Th168;
  hence thesis by GLIB_002:23;
end;

registration
  let G be non connected _Graph;
  cluster G.allSpanningTrees() -> empty;
  coherence by Th173;
end;

registration
  let G be connected _Graph;
  cluster G.allSpanningTrees() -> non empty Tree-like simple;
  coherence
  proof
    thus G.allSpanningTrees() is non empty by Th173;
    G.allSpanningTrees() = G.allSpanningSG() /\ G.allTrees() by Th169;
    hence thesis;
  end;
end;

theorem Th174:
  for G being connected _Graph, H being connected spanning Subgraph of G
  holds H.allSpanningTrees() c= G.allSpanningTrees()
proof
  let G be connected _Graph, H be connected spanning Subgraph of G;
  now
    let x be object;
    assume A1: x in H.allSpanningTrees();
    then reconsider H9 = x as plain spanning acyclic Subgraph of H by Th168;
    the_Vertices_of H9 = the_Vertices_of H by GLIB_000:def 33
      .= the_Vertices_of G by GLIB_000:def 33;
    then H9 is plain spanning acyclic Subgraph of G
      by GLIB_000:43, GLIB_000:def 33;
    hence x in G.allSpanningTrees() by A1, Th168;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th175:
  for G2 being loopless connected _Graph
  holds G2.allSpanningTrees() c= G1.allSpanningTrees()
  implies G2 is spanning Subgraph of G1
proof
  let G2 be loopless connected _Graph;
  assume A1: G2.allSpanningTrees() c= G1.allSpanningTrees();
  set H0 = the plain spanning Tree-like Subgraph of G2;
  H0 in G2.allSpanningTrees() by Th168;
  then H0 is spanning Subgraph of G1 by A1, Th168;
  then A2: the_Vertices_of G1 = the_Vertices_of H0 by GLIB_000:def 33
    .= the_Vertices_of G2 by GLIB_000:def 33;
  now
    let x be object;
    assume A3: x in the_Edges_of G2;
    x in the_Edges_of G2 \ G2.loops() by A3;
    then consider T being plain spanning Tree-like Subgraph of G2 such that
      A4: x in the_Edges_of T by Th167;
    T in G2.allSpanningTrees() by Th168;
    then T is Subgraph of G1 by A1, Th168;
    then the_Edges_of T c= the_Edges_of G1 by GLIB_000:def 32;
    hence x in the_Edges_of G1 by A4;
  end;
  then A5: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
  now
    let x be set;
    assume A6: x in the_Edges_of G2;
    x in the_Edges_of G2 \ G2.loops() by A6;
    then consider T being plain spanning Tree-like Subgraph of G2 such that
      A7: x in the_Edges_of T by Th167;
    T in G2.allSpanningTrees() by Th168;
    then A8: T is Subgraph of G1 by A1, Th168;
    thus (the_Source_of G2).x = (the_Source_of T).x by A7, GLIB_000:def 32
      .= (the_Source_of G1).x by A7, A8, GLIB_000:def 32;
    thus (the_Target_of G2).x = (the_Target_of T).x by A7, GLIB_000:def 32
      .= (the_Target_of G1).x by A7, A8, GLIB_000:def 32;
  end;
  hence thesis by A2, A5, GLIB_000:def 32, GLIB_000:def 33;
end;

theorem Th176:
  for H being removeLoops of G
  holds G.allSpanningTrees() = H.allSpanningTrees()
proof
  let H be removeLoops of G;
  per cases;
  suppose A1: G is connected;
    A2: H.allSpanningTrees() c= G.allSpanningTrees() by A1, Th174;
    now
      let x be object;
      assume A3: x in G.allSpanningTrees();
      then reconsider G2 = x as plain spanning acyclic Subgraph of G by Th168;
      A4: G2 is connected by A3, Th168;
      A5: the_Vertices_of G2 = the_Vertices_of G by GLIB_000:def 33
        .= the_Vertices_of H by GLIB_000:def 33;
      A6: the_Edges_of H = the_Edges_of G \ G.loops() by GLIB_000:53;
      the_Edges_of G2 /\ G.loops() = {}
      proof
        assume the_Edges_of G2 /\ G.loops() <> {};
        then consider y being object such that
          A7: y in the_Edges_of G2 /\ G.loops() by XBOOLE_0:def 1;
        A8: y in the_Edges_of G2 & y in G.loops() by A7, XBOOLE_0:def 4;
        then consider v being object such that
          A9: y Joins v,v,G by GLIB_009:def 2;
        y is set & v is set by TARSKI:1;
        then y Joins v,v,G2 by A8, A9, GLIB_000:73;
        then y in G2.loops() by GLIB_009:def 2;
        hence contradiction;
      end;
      then the_Edges_of G2 c= the_Edges_of H
        by A6, XBOOLE_0:def 7, XBOOLE_1:86;
      then reconsider G2 as spanning Subgraph of H by A5, GLIB_000:def 33, 44;
      G2 is Tree-like by A4;
      hence x in H.allSpanningTrees() by Th168;
    end;
    then G.allSpanningTrees() c= H.allSpanningTrees() by TARSKI:def 3;
    hence thesis by A2, XBOOLE_0:def 10;
  end;
  suppose G is non connected;
    then G.allSpanningTrees() = {} & H.allSpanningTrees() = {};
    hence thesis;
  end;
end;

theorem Th177:
  for G1, G2 being loopless connected _Graph
  holds G1 == G2 iff G1.allSpanningTrees() = G2.allSpanningTrees()
proof
  let G1, G2 be loopless connected _Graph;
  hereby
    assume G1 == G2;
    then G2 is removeLoops of G1 by GLIB_009:58;
    hence G1.allSpanningTrees() = G2.allSpanningTrees() by Th176;
  end;
  assume G1.allSpanningTrees() = G2.allSpanningTrees();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th175;
  hence thesis by GLIB_000:87;
end;

theorem
  for G1, G2 being connected _Graph
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G3 == G4 iff G1.allSpanningTrees() = G2.allSpanningTrees()
proof
  let G1, G2 be connected _Graph;
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  hereby
    assume A1: G3 == G4;
    thus G1.allSpanningTrees() = G3.allSpanningTrees() by Th176
      .= G4.allSpanningTrees() by A1, Th177
      .= G2.allSpanningTrees() by Th176;
  end;
  assume A2: G1.allSpanningTrees() = G2.allSpanningTrees();
  G3.allSpanningTrees() = G1.allSpanningTrees() by Th176
    .= G4.allSpanningTrees() by A2, Th176;
  hence thesis by Th177;
end;

theorem Th179:
  for F being PGraphMapping of G1, G2
  st F is weak_SG-embedding & rng F_V = the_Vertices_of G2
  holds rng(SG2SGFunc(F) | G1.allSpanningTrees()) c= G2.allSpanningTrees()
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  assume F is weak_SG-embedding & rng F_V = the_Vertices_of G2;
  then A1: rng(f | G1.allConnectedSG()) c= G2.allConnectedSG() &
    rng(f | G1.allSpanningForests()) c= G2.allSpanningForests()
    by Th132, Th113;
  f | G1.allSpanningTrees()
     = f | (G1.allSpanningForests() /\ G1.allConnectedSG()) by Th170
    .= (f|G1.allSpanningForests()) /\ (f|G1.allConnectedSG()) by RELAT_1:79;
  then A2: rng(f | G1.allSpanningTrees()) c=
    rng(f|G1.allSpanningForests())/\rng(f|G1.allConnectedSG()) by RELAT_1:13;
  rng(f|G1.allSpanningForests())/\rng(f|G1.allConnectedSG()) c=
    G2.allSpanningForests() /\ G2.allConnectedSG() by A1, XBOOLE_1:27;
  then rng(f | G1.allSpanningTrees()) c=
    G2.allSpanningForests() /\ G2.allConnectedSG() by A2, XBOOLE_1:1;
  hence thesis by Th170;
end;

theorem Th180:
  for F being PGraphMapping of G1, G2 st F is weak_SG-embedding onto
  holds G2.allSpanningTrees() = rng(SG2SGFunc(F) | G1.allSpanningTrees())
proof
  let F be PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  assume A1: F is weak_SG-embedding onto;
  then rng F_V = the_Vertices_of G2 by GLIB_010:def 12;
  then A2: rng(f|G1.allSpanningTrees()) c= G2.allSpanningTrees() by A1, Th179;
  G2.allConnectedSG() c= rng(f | G1.allConnectedSG()) &
    G2.allSpanningForests() c= rng(f | G1.allSpanningForests())
    by A1, Th133, Th114;
  then G2.allConnectedSG() /\ G2.allSpanningForests() c=
    rng(f | G1.allConnectedSG()) /\ rng(f | G1.allSpanningForests())
    by XBOOLE_1:27;
  then A3: G2.allSpanningTrees() c=
    rng(f | G1.allConnectedSG()) /\ rng(f | G1.allSpanningForests()) by Th170;
  A4: rng(f | G1.allConnectedSG()) = f.:G1.allConnectedSG() by RELAT_1:115;
  A5: rng(f | G1.allSpanningForests()) = f.:G1.allSpanningForests()
    by RELAT_1:115;
  A6: f is one-to-one by A1, Th31;
  rng(f | G1.allConnectedSG()) /\ rng(f | G1.allSpanningForests())
     = f.:(G1.allConnectedSG() /\ G1.allSpanningForests())
        by A4, A5, A6, FUNCT_1:62
    .= rng(f | (G1.allConnectedSG() /\ G1.allSpanningForests())) by RELAT_1:115
    .= rng(f | G1.allSpanningTrees()) by Th170;
  hence thesis by A2, A3, XBOOLE_0:def 10;
end;

theorem Th181:
  G2 is G1-Disomorphic implies
    G1.allSpanningTrees(),G2.allSpanningTrees() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allSpanningTrees();
  A2: dom f = G1.allSpanningTrees() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningTrees() by A1, Th180;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningTrees();
    then reconsider H = G as plain spanning acyclic Subgraph of G1 by Th168;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem Th182:
  G2 is G1-isomorphic implies
    G1.allSpanningTrees(),G2.allSpanningTrees() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allSpanningTrees();
  A2: dom f = G1.allSpanningTrees() by FUNCT_2:def 1;
  A3: rng f = G2.allSpanningTrees() by A1, Th180;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allSpanningTrees();
    then reconsider H = G as plain spanning acyclic Subgraph of G1 by Th168;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-Disomorphic implies
    G1.allSpanningTrees(),G2.allSpanningTrees() are_Disomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allSpanningTrees() = G3.allSpanningTrees() &
    G2.allSpanningTrees() = G4.allSpanningTrees() by Th176;
  hence thesis by Th181;
end;

theorem
  for G3 being removeLoops of G1, G4 being removeLoops of G2
  holds G4 is G3-isomorphic implies
    G1.allSpanningTrees(),G2.allSpanningTrees() are_isomorphic
proof
  let G3 be removeLoops of G1, G4 be removeLoops of G2;
  G1.allSpanningTrees() = G3.allSpanningTrees() &
    G2.allSpanningTrees() = G4.allSpanningTrees() by Th176;
  hence thesis by Th182;
end;

theorem Th185:
  for G being connected _Graph, H being removeLoops of G
  holds H is GraphUnion of G.allSpanningTrees()
proof
  let G be connected _Graph, H be removeLoops of G;
  set G9 = the GraphUnion of G.allSpanningTrees();
  reconsider G8 = G as GraphUnion of G.allSG() by Th35;
  set H9 = the GraphUnion of {H};
  now
    thus G9 is Subgraph of G8 by GLIBPRE1:119;
    now
      let x be object;
      set H8 = the Element of G.allSpanningTrees();
      assume x in the_Vertices_of H;
      then A1: x in the_Vertices_of G;
      H8 is spanning by Th168;
      then A2: x in the_Vertices_of H8 by A1, GLIB_000:def 33;
      H8 is Subgraph of G9 by GLIB_014:21;
      then the_Vertices_of H8 c= the_Vertices_of G9 by GLIB_000:def 32;
      hence x in the_Vertices_of G9 by A2;
    end;
    hence the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;
    now
      let x be object;
      assume x in the_Edges_of H;
      then x in the_Edges_of G \ G.loops() by GLIB_000:53;
      then consider T being plain spanning Tree-like Subgraph of G such that
        A3: x in the_Edges_of T by Th167;
      T in G.allSpanningTrees() by Th168;
      then T is Subgraph of G9 by GLIB_014:21;
      then the_Edges_of T c= the_Edges_of G9 by GLIB_000:def 32;
      hence x in the_Edges_of G9 by A3;
    end;
    hence the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;
  end;
  then A4: H is Subgraph of G9 by GLIB_000:44;
  now
    let H2 be Element of G.allSpanningTrees();
    reconsider H1 = H as Element of {H} by TARSKI:def 1;
    take H1;
    H.allSpanningTrees() = G.allSpanningTrees() by Th176;
    hence H2 is Subgraph of H1 by Th168;
  end;
  then G9 is Subgraph of H9 by GLIBPRE1:118;
  then G9 is Subgraph of H by GLIB_000:91, GLIB_014:24;
  hence thesis by A4, GLIB_000:87, GLIB_014:22;
end;

theorem
  for G being loopless connected _Graph
  holds G is GraphUnion of G.allSpanningTrees()
proof
  let G be loopless connected _Graph;
  set H = the removeLoops of G;
  A1: G == H by GLIB_009:58;
  H is GraphUnion of G.allSpanningTrees() by Th185;
  hence thesis by A1, GLIB_014:22;
end;

theorem
  G is Tree-like iff G.allSpanningTrees() = { G | _GraphSelectors }
proof
  hereby
    assume A1: G is Tree-like;
    now
      let x be object;
      hereby
        assume A2: x in G.allSpanningTrees();
        then reconsider G9 = x as plain spanning Subgraph of G by Th168;
        A3: G == G9 by A1, A2, GLIBPRE1:40;
        G == G | _GraphSelectors by GLIB_000:128;
        hence x = G | _GraphSelectors by A3, GLIB_000:85, GLIB_009:44;
      end;
      assume x = G | _GraphSelectors;
      hence x in G.allSpanningTrees() by A1, Th172;
    end;
    hence G.allSpanningTrees() = {G | _GraphSelectors} by TARSKI:def 1;
  end;
  assume G.allSpanningTrees() = {G | _GraphSelectors};
  then G | _GraphSelectors in G.allSpanningTrees() by TARSKI:def 1;
  then A4: G | _GraphSelectors is connected acyclic by Th168;
  G == G | _GraphSelectors by GLIB_000:128;
  hence thesis by A4, GLIB_002:48;
end;

theorem
  G is connected iff the_Vertices_of G.allSpanningTrees() = {the_Vertices_of G}
proof
  hereby
    assume A1: G is connected;
    A2: the_Vertices_of G.allSpanningForests() = { the_Vertices_of G } by Th123
;
    G.allSpanningTrees() = G.allConnectedSG()/\G.allSpanningForests() by Th170;
    then G.allSpanningTrees() c= G.allSpanningForests() by XBOOLE_1:17;
    then the_Vertices_of G.allSpanningTrees() c= { the_Vertices_of G }
      by A2, GLIBPRE1:115;
    hence the_Vertices_of G.allSpanningTrees() = { the_Vertices_of G }
      by A1, ZFMISC_1:33;
  end;
  assume the_Vertices_of G.allSpanningTrees() = { the_Vertices_of G };
  hence thesis;
end;

begin :: Component Subgraph set

definition
  let G;
  func G.allComponents() -> Subset of G.allSG() equals
  { H where H is Element of [#]G.allSG() : H is Component-like };
  coherence
  proof
    now
      let x be object;
      assume x in {H where H is Element of [#]G.allSG() : H is Component-like};
      then consider H being Element of [#]G.allSG() such that
        A1: x = H and H is Component-like;
      thus x in G.allSG() by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th189:
  G2 in G1.allComponents() iff G2 is plain Component of G1
proof
  hereby
    assume G2 in G1.allComponents();
    then consider H being Element of [#]G1.allSG() such that
      A1: G2 = H & H is Component-like;
    thus G2 is plain Component of G1 by A1;
  end;
  assume A2: G2 is plain Component of G1;
  then G2 in [#]G1.allSG() by Th1;
  hence thesis by A2;
end;

theorem
  G.allComponents() c= G.allInducedSG() /\ G.allConnectedSG()
proof
  now
    let x be object;
    assume x in G.allComponents();
    then reconsider C = x as plain Component of G by Th189;
    set v = the Vertex of C;
    the_Vertices_of C c= the_Vertices_of G;
    then reconsider v as Vertex of G by TARSKI:def 3;
    set C9 = the plain inducedSubgraph of G,G.reachableFrom(v);
    the_Vertices_of C9 = G.reachableFrom(v) by GLIB_000:def 37
      .= the_Vertices_of C by GLIB_002:33;
    then C = C9 by GLIB_002:32, GLIB_009:44;
    then x in G.allInducedSG() & x in G.allConnectedSG() by Th124;
    hence x in G.allInducedSG() /\ G.allConnectedSG() by XBOOLE_0:def 4;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th191:
  for H being Component of G holds H | _GraphSelectors in G.allComponents()
proof
  let H be Component of G;
  H | _GraphSelectors == H by GLIB_000:128;
  then H | _GraphSelectors is Component of G by GLIBPRE1:38;
  hence thesis by Th189;
end;

theorem Th192:
  G is connected iff G | _GraphSelectors in G.allComponents()
proof
  hereby
    assume G is connected;
    then G is Component of G by GLIB_002:30;
    hence G | _GraphSelectors in G.allComponents() by Th191;
  end;
  assume G | _GraphSelectors in G.allComponents();
  then G | _GraphSelectors is Component of G by Th189;
  hence G is connected by GLIB_000:128, GLIBPRE1:38;
end;

Lm3:
  the_Vertices_of G.allComponents() = G.componentSet()
proof
  now
    let V be object;
    hereby
      assume V in G.componentSet();
      then consider v being Vertex of G such that
        A1: V = G.reachableFrom(v) by GLIB_002:def 8;
      set C = the plain inducedSubgraph of G, G.reachableFrom(v);
      reconsider C as _Graph;
      take C;
      thus C in G.allComponents() by Th189;
      thus V = the_Vertices_of C by A1, GLIB_000:def 37;
    end;
    given C being _Graph such that
      A2: C in G.allComponents() & V = the_Vertices_of C;
    set v = the Vertex of C;
    A3: C is plain Component of G by A2, Th189;
    then the_Vertices_of C c= the_Vertices_of G by GLIB_000:def 32;
    then reconsider v as Vertex of G by TARSKI:def 3;
    set C9 = the plain inducedSubgraph of G,G.reachableFrom(v);
    A4: the_Vertices_of C9 = G.reachableFrom(v) by GLIB_000:def 37;
    then the_Vertices_of C9 = the_Vertices_of C by A3, GLIB_002:33;
    then C = C9 by A3, GLIB_002:32, GLIB_009:44;
    hence V in G.componentSet() by A2, A4, GLIB_002:def 8;
  end;
  hence thesis by GLIB_014:def 14;
end;

registration
  let G;
  cluster G.allComponents() -> non empty vertex-disjoint edge-disjoint
    \/-tolerating plain connected;
  coherence
  proof
    the plain Component of G in G.allComponents() by Th189;
    hence G.allComponents() is non empty;
    now
      let G1, G2 be _Graph;
      set V1 = the_Vertices_of G1, V2 = the_Vertices_of G2;
      assume A1: G1 in G.allComponents() & G2 in G.allComponents() & G1 <> G2;
      then V1 in the_Vertices_of G.allComponents() &
        V2 in the_Vertices_of G.allComponents() by GLIB_014:def 14;
      then A2: V1 in G.componentSet() & V2 in G.componentSet() by Lm3;
      A3: G.componentSet() is a_partition of the_Vertices_of G by GLIB_008:23;
      V1 <> V2
      proof
        assume A4: V1 = V2;
        G1 is Component of G & G2 is Component of G by A1, Th189;
        hence contradiction by A1, A4, GLIB_002:32, GLIB_009:44;
      end;
      hence V1 misses V2 by A2, A3, EQREL_1:def 4;
    end;
    hence G.allComponents() is vertex-disjoint by GLIB_015:def 18;
    hence G.allComponents() is edge-disjoint;
    thus G.allComponents() is \/-tolerating plain;
    for H being _Graph st H in G.allComponents() holds H is connected by Th189;
    hence G.allComponents() is connected by GLIB_014:def 9;
  end;
end;

theorem Th193:
  G2.allComponents() c= G1.allComponents() implies G2 is Subgraph of G1
proof
  assume A1: G2.allComponents() c= G1.allComponents();
  now
    now
      let x be object;
      assume x in the_Vertices_of G2;
      then reconsider v = x as Vertex of G2;
      set C = the plain inducedSubgraph of G2, G2.reachableFrom(v);
      C in G2.allComponents() by Th189;
      then C is Component of G1 by A1, Th189;
      then A2: the_Vertices_of C c= the_Vertices_of G1 by GLIB_000:def 32;
      the_Vertices_of C = G2.reachableFrom(v) by GLIB_000:def 37;
      then v in the_Vertices_of C by GLIB_002:9;
      hence x in the_Vertices_of G1 by A2;
    end;
    hence the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
    now
      let e be object;
      set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
      assume e in the_Edges_of G2;
      then A3: e Joins v,w,G2 by GLIB_000:def 13;
      then reconsider v as Vertex of G2 by GLIB_000:13;
      set H = the plain inducedSubgraph of G2, G2.reachableFrom(v);
      the_Vertices_of H = G2.reachableFrom(v) by GLIB_000:def 37;
      then reconsider v9 = v as Vertex of H by GLIB_002:9;
      e in v.edgesInOut() by A3, GLIB_000:62;
      then e in v9.edgesInOut() by GLIBPRE0:44;
      then A4: e in the_Edges_of H;
      H in G2.allComponents() by Th189;
      then H is Subgraph of G1 by A1, Th189;
      then the_Edges_of H c= the_Edges_of G1 by GLIB_000:def 32;
      hence e in the_Edges_of G1 by A4;
    end;
    hence the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
    let e be set;
    set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
    assume e in the_Edges_of G2;
    then A5: e DJoins v,w,G2 by GLIB_000:def 14;
    then e Joins v,w,G2 by GLIB_000:16;
    then reconsider v as Vertex of G2 by GLIB_000:13;
    set H = the plain inducedSubgraph of G2, G2.reachableFrom(v);
    the_Vertices_of H = G2.reachableFrom(v) by GLIB_000:def 37;
    then reconsider v9 = v as Vertex of H by GLIB_002:9;
    e in v.edgesOut() by A5, GLIB_000:59;
    then e in v9.edgesOut() by GLIBPRE0:44;
    then A6: e DJoins v,w,H by A5, GLIB_000:73;
    H in G2.allComponents() by Th189;
    then H is Subgraph of G1 by A1, Th189;
    then e DJoins v,w,G1 by A6, GLIB_000:72;
    hence (the_Source_of G2).e = (the_Source_of G1).e &
      (the_Target_of G2).e = (the_Target_of G1).e by GLIB_000:def 14;
  end;
  hence thesis by GLIB_000:def 32;
end;

theorem
  G1 == G2 iff G1.allComponents() = G2.allComponents()
proof
  hereby
    assume A1: G1 == G2;
    now
      let x be object;
      hereby
        assume x in G1.allComponents();
        then reconsider C = x as plain Component of G1 by Th189;
        C is Component of G2 by A1, GLIBPRE1:39;
        hence x in G2.allComponents() by Th189;
      end;
      assume x in G2.allComponents();
      then reconsider C = x as plain Component of G2 by Th189;
      C is Component of G1 by A1, GLIBPRE1:39;
      hence x in G1.allComponents() by Th189;
    end;
    hence G1.allComponents() = G2.allComponents() by TARSKI:2;
  end;
  assume G1.allComponents() = G2.allComponents();
  then G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th193;
  hence thesis by GLIB_000:87;
end;

theorem Th195:
  for F being non empty one-to-one PGraphMapping of G1, G2 st F is isomorphism
  holds G2.allComponents() = rng(SG2SGFunc(F) | G1.allComponents())
proof
  let F be non empty one-to-one PGraphMapping of G1, G2;
  set f = SG2SGFunc(F);
  A1: dom(f | G1.allComponents()) = G1.allComponents() by FUNCT_2:def 1;
  assume A2: F is isomorphism;
  now
    let y be object;
    hereby
      assume y in G2.allComponents();
      then reconsider C2 = y as plain Component of G2 by Th189;
      set v2 = the Vertex of C2;
      the_Vertices_of C2 c= the_Vertices_of G2;
      then reconsider v2 as Vertex of G2 by TARSKI:def 3;
      A3: the_Vertices_of C2 = G2.reachableFrom(v2) by GLIB_002:33;
      the_Edges_of C2 = G2.edgesBetween(the_Vertices_of C2) by GLIB_002:31;
      then A4: C2 is inducedSubgraph of G2, G2.reachableFrom(v2)
        by A3, GLIB_000:170;
      A5: G2 == rng F by A2, GLIB_010:56;
      then G2.edgesBetween(G2.reachableFrom(v2)) =
        (rng F).edgesBetween(G2.reachableFrom(v2)) by GLIB_000:90;
      then reconsider C2 as inducedSubgraph of rng F, G2.reachableFrom(v2)
        by A4, A5, GLIB_000:95;
      set C1 = the plain inducedSubgraph of G1, F_V"the_Vertices_of C2;
      A6: dom F_E = the_Edges_of G1 by A2, GLIB_010:def 11;
      the_Vertices_of G2 = the_Vertices_of rng F by A5, GLIB_000:def 34;
      then A7: C2 = rng(F | C1) by A6, GLIB_009:44, GLIBPRE1:101
        .= f.C1 by Def5;
      rng F_V = the_Vertices_of G2 by A2, GLIB_010:def 12;
      then consider v1 being object such that
        A8: v1 in dom F_V & F_V.v1 = v2 by FUNCT_1:def 3;
      reconsider v1 as Vertex of G1 by A8;
      F_V"the_Vertices_of C2 = G1.reachableFrom(v1) by A2, A3, A8, GLIBPRE1:97;
      then C1 in dom(f | G1.allComponents()) & C2 = (f | G1.allComponents()).C1
        by A1, A7, Th189, FUNCT_1:49;
      hence y in rng(f | G1.allComponents()) by FUNCT_1:def 3;
    end;
    assume y in rng(f | G1.allComponents());
    then consider x being object such that
      A9: x in dom(f | G1.allComponents()) & (f | G1.allComponents()).x = y
      by FUNCT_1:def 3;
    reconsider C1 = x as plain Component-like Subgraph of G1 by A9, Th189;
    set v1 = the Vertex of C1;
    the_Vertices_of C1 c= the_Vertices_of G1;
    then reconsider v1 as Vertex of G1 by TARSKI:def 3;
    A10: y = f.C1 by A9, FUNCT_1:47
      .= rng(F | C1) by Def5;
    dom F_V = the_Vertices_of G1 by A2, GLIB_010:def 11;
    then F_V.v1 in rng F_V by FUNCT_1:3;
    then reconsider v2 = F_V.v1 as Vertex of G2;
    A11: F_V.:the_Vertices_of C1 = F_V.:(G1.reachableFrom(v1)) by GLIB_002:33
      .= G2.reachableFrom(v2) by A2, GLIBPRE1:81;
    A12: rng (F | C1)_V = G2.reachableFrom(v2) by A11, RELAT_1:115;
    rng (F | C1)_E = F_E.:the_Edges_of C1 by RELAT_1:115
      .= F_E.:(G1.edgesBetween(the_Vertices_of C1)) by GLIB_002:31
      .= G2.edgesBetween(G2.reachableFrom(v2)) by A2, A11, GLIBPRE1:93;
    hence y in G2.allComponents() by A10, A12, Th189;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  G2 is G1-Disomorphic implies
    G1.allComponents(),G2.allComponents() are_Disomorphic
proof
  assume G2 is G1-Disomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is Disomorphism by GLIB_010:def 24;
  set f = SG2SGFunc(F) | G1.allComponents();
  A2: dom f = G1.allComponents() by FUNCT_2:def 1;
  A3: rng f = G2.allComponents() by A1, Th195;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allComponents();
    then reconsider H = G as plain Component-like Subgraph of G1 by Th189;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is Disomorphism by A1, GLIBPRE1:110;
    hence f.G is G-Disomorphic _Graph
      by A6, GLIB_010:def 24;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 12;
end;

theorem
  G2 is G1-isomorphic implies
    G1.allComponents(),G2.allComponents() are_isomorphic
proof
  assume G2 is G1-isomorphic;
  then consider F being PGraphMapping of G1, G2 such that
    A1: F is isomorphism by GLIB_010:def 23;
  set f = SG2SGFunc(F) | G1.allComponents();
  A2: dom f = G1.allComponents() by FUNCT_2:def 1;
  A3: rng f = G2.allComponents() by A1, Th195;
  SG2SGFunc(F) is one-to-one by A1, Th31;
  then A4: f is one-to-one by FUNCT_1:52;
  now
    let G be _Graph;
    assume A5: G in G1.allComponents();
    then reconsider H = G as plain Component-like Subgraph of G1 by Th189;
    reconsider F9 = F|H as PGraphMapping of H, rng(F|H) by GLIBPRE1:88;
    A6: f.G = (SG2SGFunc F).G by A5, FUNCT_1:49
      .= rng(F | H) by Def5;
    F9 is isomorphism by A1, GLIBPRE1:110;
    hence f.G is G-isomorphic _Graph
      by A6, GLIB_010:def 23;
  end;
  hence thesis by A2, A3, A4, GLIB_015:def 13;
end;

theorem Th198:
  G is GraphUnion of G.allComponents()
proof
  set G9 = the GraphUnion of G.allComponents();
  G is GraphUnion of G.allSG() by Th35;
  then A1: G9 is Subgraph of G by GLIBPRE1:119;
  A2: now
    let v be Vertex of G;
    set H9 = the plain inducedSubgraph of G,G.reachableFrom(v);
    reconsider H9 as Element of G.allComponents() by Th189;
    take H9;
    the_Vertices_of H9 = G.reachableFrom(v) by GLIB_000:def 37;
    hence v in the_Vertices_of H9 by GLIB_002:9;
  end;
  now
    per cases;
    suppose G is edgeless;
      hence G is Subgraph of G9 by A2, Th22;
    end;
    suppose G is non edgeless;
      then reconsider G0 = G as non edgeless _Graph;
      now
        let e be Edge of G0;
        set v = (the_Source_of G).e, w = (the_Target_of G).e;
        e DJoins v,w,createGraph(e) by Th14;
        then e Joins v,w,createGraph(e) by GLIB_000:16;
        then A3: e Joins v,w,G by GLIB_000:72;
        then reconsider v,w as Vertex of G by GLIB_000:13;
        set H9 = the plain inducedSubgraph of G,G.reachableFrom(v);
        reconsider H9 as Element of G.allComponents() by Th189;
        take H9;
        A4: the_Vertices_of H9 = G.reachableFrom(v) by GLIB_000:def 37;
        then A5: v in the_Vertices_of H9 by GLIB_002:9;
        then A6: w in the_Vertices_of H9 by A3, A4, GLIB_002:10;
        then e in G.edgesBetween(the_Vertices_of H9) by A3, A5, GLIB_000:32;
        then e in the_Edges_of H9 by A4, GLIB_000:def 37;
        then {e} c= the_Edges_of H9 by ZFMISC_1:31;
        then A7: the_Edges_of createGraph(e) c= the_Edges_of H9 by Th13;
        {v,w} c= the_Vertices_of H9 by A5, A6, ZFMISC_1:32;
        then the_Vertices_of createGraph(e) c= the_Vertices_of H9 by Th13;
        hence createGraph(e) is Subgraph of H9 by A7, GLIB_000:44;
      end;
      hence G is Subgraph of G9 by A2, Th23;
    end;
  end;
  hence thesis by A1, GLIB_000:87, GLIB_014:22;
end;

theorem Th199:
  (G is loopless iff G.allComponents() is loopless) &
  (G is non-multi iff G.allComponents() is non-multi) &
  (G is non-Dmulti iff G.allComponents() is non-Dmulti) &
  (G is simple iff G.allComponents() is simple) &
  (G is Dsimple iff G.allComponents() is Dsimple) &
  (G is acyclic iff G.allComponents() is acyclic) &
  (G is edgeless iff G.allComponents() is edgeless) &
  (G is chordal iff G.allComponents() is chordal) &
  (G is loopfull iff G.allComponents() is loopfull)
proof
  A1: G is GraphUnion of G.allComponents() by Th198;
  thus G is loopless iff G.allComponents() is loopless by A1;
  thus G is non-multi iff G.allComponents() is non-multi by A1;
  thus G is non-Dmulti iff G.allComponents() is non-Dmulti by A1;
  thus G is simple iff G.allComponents() is simple by A1;
  thus G is Dsimple iff G.allComponents() is Dsimple by A1;
  thus G is acyclic iff G.allComponents() is acyclic by A1;
  thus G is edgeless iff G.allComponents() is edgeless by A1;
  thus G is chordal iff G.allComponents() is chordal by A1 ,GLIB_015:63;
  thus G is loopfull iff G.allComponents() is loopfull by A1, GLIB_015:63;
end;

registration
  let G be loopless _Graph;
  cluster G.allComponents() -> loopless;
  coherence;
end;

registration
  let G be non-multi _Graph;
  cluster G.allComponents() -> non-multi;
  coherence;
end;

registration
  let G be non-Dmulti _Graph;
  cluster G.allComponents() -> non-Dmulti;
  coherence;
end;

registration
  let G be simple _Graph;
  cluster G.allComponents() -> simple;
  coherence;
end;

registration
  let G be Dsimple _Graph;
  cluster G.allComponents() -> Dsimple;
  coherence;
end;

registration
  let G be acyclic _Graph;
  cluster G.allComponents() -> acyclic;
  coherence;
end;

registration
  let G be edgeless _Graph;
  cluster G.allComponents() -> edgeless;
  coherence;
end;

registration
  let G be chordal _Graph;
  cluster G.allComponents() -> chordal;
  coherence by Th199;
end;

registration
  let G be loopfull _Graph;
  cluster G.allComponents() -> loopfull;
  coherence by Th199;
end;

theorem
  G is connected iff G.allComponents() = { G | _GraphSelectors }
proof
  hereby
    assume A1: G is connected;
    then A2: { G | _GraphSelectors } c= G.allComponents()
      by Th192, ZFMISC_1:31;
    now
      let x be object;
      assume x in G.allComponents();
      then reconsider H = x as plain Component of G by Th189;
      A3: G == H by A1, GLIB_006:55;
      G == G | _GraphSelectors by GLIB_000:128;
      then H = G | _GraphSelectors by A3, GLIB_000:85, GLIB_009:44;
      hence x in { G | _GraphSelectors } by TARSKI:def 1;
    end;
    then G.allComponents() c= { G | _GraphSelectors } by TARSKI:def 3;
    hence G.allComponents() = { G | _GraphSelectors } by A2, XBOOLE_0:def 10;
  end;
  assume { G | _GraphSelectors } = G.allComponents();
  then G | _GraphSelectors in G.allComponents() by TARSKI:def 1;
  hence G is connected by Th192;
end;

theorem
  the_Vertices_of G.allComponents() = G.componentSet() by Lm3;

theorem
  G.numComponents() = card G.allComponents()
proof
  defpred P[object, object] means ex H being plain Component of G st
    $1 = H & $2 = the_Vertices_of H;
  A1: for x,y1,y2 being object st x in G.allComponents() & P[x,y1] & P[x,y2]
    holds y1 = y2;
  A2: for x being object st x in G.allComponents() ex y being object st P[x,y]
  proof
    let x be object;
    assume x in G.allComponents();
    then reconsider H = x as plain Component of G by Th189;
    take the_Vertices_of H, H;
    thus thesis;
  end;
  consider f being Function such that
    A3: dom f = G.allComponents() and
    A4: for x being object st x in G.allComponents() holds P[x,f.x]
    from FUNCT_1:sch 2(A1,A2);
  now
    let y be object;
    thus y in G.componentSet() implies
      ex x being object st x in dom f & y = f.x
    proof
      assume y in G.componentSet();
      then consider v being Vertex of G such that
        A5: y = G.reachableFrom(v) by GLIB_002:def 8;
      set H = the plain inducedSubgraph of G, G.reachableFrom(v);
      take H;
      thus H in dom f by A3, Th189;
      then consider H9 being plain Component of G such that
        A6: H = H9 & f.H = the_Vertices_of H9 by A3, A4;
      thus y = f.H by A5, A6, GLIB_000:def 37;
    end;
    given x being object such that
      A7: x in dom f & y = f.x;
    consider H being plain Component of G such that
      A8: x = H & y = the_Vertices_of H by A3, A4, A7;
    set v = the Vertex of H;
    the_Vertices_of H c= the_Vertices_of G;
    then reconsider v as Vertex of G by TARSKI:def 3;
    the_Vertices_of H = G.reachableFrom(v) by GLIB_002:33;
    hence y in G.componentSet() by A8, GLIB_002:def 8;
  end;
  then A9: rng f = G.componentSet() by FUNCT_1:def 3;
  now
    let x1,x2 be object;
    assume A10: x1 in dom f & x2 in dom f & f.x1 = f.x2;
    then consider H1 being plain Component of G such that
      A11: x1 = H1 & f.x1 = the_Vertices_of H1 by A3, A4;
    consider H2 being plain Component of G such that
      A12: x2 = H2 & f.x2 = the_Vertices_of H2 by A3, A4, A10;
    thus x1 = x2 by A10, A11, A12, GLIB_002:32, GLIB_009:44;
  end;
  then card G.allComponents() = card G.componentSet()
    by A3, A9, FUNCT_1:def 4, CARD_1:70;
  hence thesis by GLIB_002:def 9;
end;