:: Alternative Graph Structures
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

registration
cluster Relation-like NAT -defined Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is finite & b1 is NAT -defined )
proofend;
end;

definition
mode GraphStruct is NAT -defined finite Function;
end;

definition
func VertexSelector  ->  Element of NAT  equals :: GLIB_000:def 1
1;
coherence
 1 is Element of NAT ;
func EdgeSelector  ->  Element of NAT  equals :: GLIB_000:def 2
2;
coherence
 2 is Element of NAT ;
func SourceSelector  ->  Element of NAT  equals :: GLIB_000:def 3
3;
coherence
 3 is Element of NAT ;
func TargetSelector  ->  Element of NAT  equals :: GLIB_000:def 4
4;
coherence
 4 is Element of NAT ;
end;

:: deftheorem  defines VertexSelector GLIB_000:def_1_:_
 VertexSelector = 1;

:: deftheorem  defines EdgeSelector GLIB_000:def_2_:_
 EdgeSelector = 2;

:: deftheorem  defines SourceSelector GLIB_000:def_3_:_
 SourceSelector = 3;

:: deftheorem  defines TargetSelector GLIB_000:def_4_:_
 TargetSelector = 4;

definition
func _GraphSelectors  ->  non empty Subset of NAT equals :: GLIB_000:def 5
{VertexSelector,EdgeSelector,SourceSelector,TargetSelector};
coherence
 {VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty Subset of NAT ;
end;

:: deftheorem  defines _GraphSelectors GLIB_000:def_5_:_
 _GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

definition
let G be GraphStruct;
func the_Vertices_of G ->  set  equals :: GLIB_000:def 6
G . VertexSelector;
coherence
 G . VertexSelector is set ;
func the_Edges_of G ->  set  equals :: GLIB_000:def 7
G . EdgeSelector;
coherence
 G . EdgeSelector is set ;
func the_Source_of G ->  set  equals :: GLIB_000:def 8
G . SourceSelector;
coherence
 G . SourceSelector is set ;
func the_Target_of G ->  set  equals :: GLIB_000:def 9
G . TargetSelector;
coherence
 G . TargetSelector is set ;
end;

:: deftheorem  defines the_Vertices_of GLIB_000:def_6_:_
 for G being GraphStruct holds the_Vertices_of G = G . VertexSelector;

:: deftheorem  defines the_Edges_of GLIB_000:def_7_:_
 for G being GraphStruct holds the_Edges_of G = G . EdgeSelector;

:: deftheorem  defines the_Source_of GLIB_000:def_8_:_
 for G being GraphStruct holds the_Source_of G = G . SourceSelector;

:: deftheorem  defines the_Target_of GLIB_000:def_9_:_
 for G being GraphStruct holds the_Target_of G = G . TargetSelector;

definition
let G be GraphStruct;
attrG is [Graph-like]  means :Def10: :: GLIB_000:def 10
( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) & the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) );
end;

:: deftheorem Def10 defines [Graph-like] GLIB_000:def_10_:_
 for G being GraphStruct holds
( G is [Graph-like] iff ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) & the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) ) );

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] for set ;
existence
 ex b1 being GraphStruct st b1 is [Graph-like]
proofend;
end;

definition
mode _Graph is [Graph-like] GraphStruct;
end;

registration
let G be _Graph;
cluster the_Vertices_of G ->  non empty ;
coherence
 not the_Vertices_of G is empty by Def10;
end;

definition
let G be _Graph;
:: original:the_Source_of
redefine func the_Source_of G ->  Function of (the_Edges_of G),(the_Vertices_of G);
coherence
 the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;
:: original:the_Target_of
redefine func the_Target_of G ->  Function of (the_Edges_of G),(the_Vertices_of G);
coherence
 the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;
end;

definition
let V be non empty set ;
let E be set ;
let S, T be Function of E,V;
func createGraph (V,E,S,T) ->  _Graph equals :: GLIB_000:def 11
<*V,E,S,T*>;
coherence
 <*V,E,S,T*> is _Graph
proofend;
end;

:: deftheorem  defines createGraph GLIB_000:def_11_:_
 for V being non empty set
for E being set
for S, T being Function of E,V holds createGraph (V,E,S,T) = <*V,E,S,T*>;

definition
let G be GraphStruct;
let n be Nat;
let x be set ;
funcG .set (n,x) ->  GraphStruct equals :: GLIB_000:def 12
G +* (n .--> x);
coherence
 G +* (n .--> x) is GraphStruct
proofend;
end;

:: deftheorem  defines .set GLIB_000:def_12_:_
 for G being GraphStruct
for n being Nat
for x being set holds G .set (n,x) = G +* (n .--> x);

Lm1:  for GS being GraphStruct holds
( GS is [Graph-like] iff ( _GraphSelectors c= dom GS &amp; not the_Vertices_of GS is empty &amp; the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) &amp; the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) )
proofend;

registration
let G be _Graph;
clusterG | _GraphSelectors ->  [Graph-like] ;
coherence
 G | _GraphSelectors is [Graph-like]
proofend;
end;

definition
let G be _Graph;
let x, y, e be set ;
prede Joins x,y,G means :Def13: :: GLIB_000:def 13
( e in the_Edges_of G &amp; ( ( (the_Source_of G) . e = x &amp; (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y &amp; (the_Target_of G) . e = x ) ) );
end;

:: deftheorem Def13 defines Joins GLIB_000:def_13_:_
 for G being _Graph
for x, y, e being set holds
( e Joins x,y,G iff ( e in the_Edges_of G &amp; ( ( (the_Source_of G) . e = x &amp; (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y &amp; (the_Target_of G) . e = x ) ) ) );

definition
let G be _Graph;
let x, y, e be set ;
prede DJoins x,y,G means :Def14: :: GLIB_000:def 14
( e in the_Edges_of G &amp; (the_Source_of G) . e = x &amp; (the_Target_of G) . e = y );
end;

:: deftheorem Def14 defines DJoins GLIB_000:def_14_:_
 for G being _Graph
for x, y, e being set holds
( e DJoins x,y,G iff ( e in the_Edges_of G &amp; (the_Source_of G) . e = x &amp; (the_Target_of G) . e = y ) );

definition
let G be _Graph;
let X, Y, e be set ;
prede SJoins X,Y,G means :Def15: :: GLIB_000:def 15
( e in the_Edges_of G &amp; ( ( (the_Source_of G) . e in X &amp; (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y &amp; (the_Target_of G) . e in X ) ) );
prede DSJoins X,Y,G means :Def16: :: GLIB_000:def 16
( e in the_Edges_of G &amp; (the_Source_of G) . e in X &amp; (the_Target_of G) . e in Y );
end;

:: deftheorem Def15 defines SJoins GLIB_000:def_15_:_
 for G being _Graph
for X, Y, e being set holds
( e SJoins X,Y,G iff ( e in the_Edges_of G &amp; ( ( (the_Source_of G) . e in X &amp; (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y &amp; (the_Target_of G) . e in X ) ) ) );

:: deftheorem Def16 defines DSJoins GLIB_000:def_16_:_
 for G being _Graph
for X, Y, e being set holds
( e DSJoins X,Y,G iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X &amp; (the_Target_of G) . e in Y ) );

Lm2:  for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )
proofend;

definition
let G be _Graph;
attrG is finite  means :Def17: :: GLIB_000:def 17
( the_Vertices_of G is finite &amp; the_Edges_of G is finite );
attrG is loopless  means :Def18: :: GLIB_000:def 18
 for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e );
attrG is trivial  means :Def19: :: GLIB_000:def 19
 card (the_Vertices_of G) = 1;
attrG is non-multi  means :Def20: :: GLIB_000:def 20
 for e1, e2, v1, v2 being set st e1 Joins v1,v2,G &amp; e2 Joins v1,v2,G holds
e1 = e2;
attrG is non-Dmulti  means :Def21: :: GLIB_000:def 21
 for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G &amp; e2 DJoins v1,v2,G holds
e1 = e2;
end;

:: deftheorem Def17 defines finite GLIB_000:def_17_:_
 for G being _Graph holds
( G is finite iff ( the_Vertices_of G is finite &amp; the_Edges_of G is finite ) );

:: deftheorem Def18 defines loopless GLIB_000:def_18_:_
 for G being _Graph holds
( G is loopless iff for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );

:: deftheorem Def19 defines trivial GLIB_000:def_19_:_
 for G being _Graph holds
( G is trivial iff card (the_Vertices_of G) = 1 );

:: deftheorem Def20 defines non-multi GLIB_000:def_20_:_
 for G being _Graph holds
( G is non-multi iff for e1, e2, v1, v2 being set st e1 Joins v1,v2,G &amp; e2 Joins v1,v2,G holds
e1 = e2 );

:: deftheorem Def21 defines non-Dmulti GLIB_000:def_21_:_
 for G being _Graph holds
( G is non-Dmulti iff for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G &amp; e2 DJoins v1,v2,G holds
e1 = e2 );

definition
let G be _Graph;
attrG is simple  means :Def22: :: GLIB_000:def 22
( G is loopless &amp; G is non-multi );
attrG is Dsimple  means :Def23: :: GLIB_000:def 23
( G is loopless &amp; G is non-Dmulti );
end;

:: deftheorem Def22 defines simple GLIB_000:def_22_:_
 for G being _Graph holds
( G is simple iff ( G is loopless &amp; G is non-multi ) );

:: deftheorem Def23 defines Dsimple GLIB_000:def_23_:_
 for G being _Graph holds
( G is Dsimple iff ( G is loopless &amp; G is non-Dmulti ) );

Lm3:  for G being _Graph st the_Edges_of G = {} holds
G is simple
proofend;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] non-multi  ->  non-Dmulti for set ;
coherence
 for b1 being _Graph st b1 is non-multi holds
b1 is non-Dmulti
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] simple  ->  loopless non-multi for set ;
coherence
 for b1 being _Graph st b1 is simple holds
( b1 is loopless &amp; b1 is non-multi ) by Def22;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-multi  ->  simple for set ;
coherence
 for b1 being _Graph st b1 is loopless &amp; b1 is non-multi holds
b1 is simple by Def22;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-Dmulti  ->  Dsimple for set ;
coherence
 for b1 being _Graph st b1 is loopless &amp; b1 is non-Dmulti holds
b1 is Dsimple by Def23;
cluster Relation-like NAT -defined Function-like finite [Graph-like] Dsimple  ->  loopless non-Dmulti for set ;
coherence
 for b1 being _Graph st b1 is Dsimple holds
( b1 is loopless &amp; b1 is non-Dmulti ) by Def23;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless trivial  ->  finite for set ;
coherence
 for b1 being _Graph st b1 is trivial &amp; b1 is loopless holds
b1 is finite
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial non-Dmulti  ->  finite for set ;
coherence
 for b1 being _Graph st b1 is trivial &amp; b1 is non-Dmulti holds
b1 is finite
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple for set ;
existence
 ex b1 being _Graph st
( b1 is trivial &amp; b1 is simple )
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial simple for set ;
existence
 ex b1 being _Graph st
( b1 is finite &amp; not b1 is trivial &amp; b1 is simple )
proofend;
end;

registration
let G be finite _Graph;
cluster the_Vertices_of G ->  finite ;
coherence
 the_Vertices_of G is finite by Def17;
cluster the_Edges_of G ->  finite ;
coherence
 the_Edges_of G is finite by Def17;
end;

registration
let G be trivial _Graph;
cluster the_Vertices_of G ->  finite ;
coherence
 the_Vertices_of G is finite
proofend;
end;

registration
let V be non empty finite set ;
let E be finite set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) ->  finite ;
coherence
 createGraph (V,E,S,T) is finite
proofend;
end;

registration
let V be non empty set ;
let E be empty set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) ->  simple ;
coherence
 createGraph (V,E,S,T) is simple
proofend;
end;

registration
let v, E be set ;
let S, T be Function of E,{v};
cluster createGraph ({v},E,S,T) ->  trivial ;
coherence
 createGraph ({v},E,S,T) is trivial
proofend;
end;

definition
let G be _Graph;
funcG .order()  ->  Cardinal equals :: GLIB_000:def 24
 card (the_Vertices_of G);
coherence
 card (the_Vertices_of G) is Cardinal ;
end;

:: deftheorem  defines .order() GLIB_000:def_24_:_
 for G being _Graph holds G .order() = card (the_Vertices_of G);

definition
let G be finite _Graph;
:: original:.order()
redefine funcG .order()  ->  non empty Element of NAT ;
coherence
 G .order() is non empty Element of NAT
proofend;
end;

definition
let G be _Graph;
funcG .size()  ->  Cardinal equals :: GLIB_000:def 25
 card (the_Edges_of G);
coherence
 card (the_Edges_of G) is Cardinal ;
end;

:: deftheorem  defines .size() GLIB_000:def_25_:_
 for G being _Graph holds G .size() = card (the_Edges_of G);

definition
let G be finite _Graph;
:: original:.size()
redefine funcG .size()  ->  Element of NAT ;
coherence
 G .size() is Element of NAT
proofend;
end;

definition
let G be _Graph;
let X be set ;
funcG .edgesInto X ->  Subset of (the_Edges_of G) means :Def26: :: GLIB_000:def 26
 for e being set holds
( e in it iff ( e in the_Edges_of G &amp; (the_Target_of G) . e in X ) );
existence
 ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff ( e in the_Edges_of G &amp; (the_Target_of G) . e in X ) )
proofend;
uniqueness
 for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff ( e in the_Edges_of G &amp; (the_Target_of G) . e in X ) ) ) &amp; ( for e being set holds
( e in b2 iff ( e in the_Edges_of G &amp; (the_Target_of G) . e in X ) ) ) holds
b1 = b2
proofend;
funcG .edgesOutOf X ->  Subset of (the_Edges_of G) means :Def27: :: GLIB_000:def 27
 for e being set holds
( e in it iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X ) );
existence
 ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X ) )
proofend;
uniqueness
 for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X ) ) ) &amp; ( for e being set holds
( e in b2 iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines .edgesInto GLIB_000:def_26_:_
 for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesInto X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G &amp; (the_Target_of G) . e in X ) ) );

:: deftheorem Def27 defines .edgesOutOf GLIB_000:def_27_:_
 for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesOutOf X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G &amp; (the_Source_of G) . e in X ) ) );

definition
let G be _Graph;
let X be set ;
funcG .edgesInOut X ->  Subset of (the_Edges_of G) equals :: GLIB_000:def 28
(G .edgesInto X) \/ (G .edgesOutOf X);
coherence
 (G .edgesInto X) \/ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;
funcG .edgesBetween X ->  Subset of (the_Edges_of G) equals :: GLIB_000:def 29
(G .edgesInto X) /\ (G .edgesOutOf X);
coherence
 (G .edgesInto X) /\ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;
end;

:: deftheorem  defines .edgesInOut GLIB_000:def_28_:_
 for G being _Graph
for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X);

:: deftheorem  defines .edgesBetween GLIB_000:def_29_:_
 for G being _Graph
for X being set holds G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X);

definition
let G be _Graph;
let X, Y be set ;
funcG .edgesBetween (X,Y) ->  Subset of (the_Edges_of G) means :Def30: :: GLIB_000:def 30
 for e being set holds
( e in it iff e SJoins X,Y,G );
existence
 ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e SJoins X,Y,G )
proofend;
uniqueness
 for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e SJoins X,Y,G ) ) &amp; ( for e being set holds
( e in b2 iff e SJoins X,Y,G ) ) holds
b1 = b2
proofend;
funcG .edgesDBetween (X,Y) ->  Subset of (the_Edges_of G) means :Def31: :: GLIB_000:def 31
 for e being set holds
( e in it iff e DSJoins X,Y,G );
existence
 ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e DSJoins X,Y,G )
proofend;
uniqueness
 for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e DSJoins X,Y,G ) ) &amp; ( for e being set holds
( e in b2 iff e DSJoins X,Y,G ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def30 defines .edgesBetween GLIB_000:def_30_:_
 for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesBetween (X,Y) iff for e being set holds
( e in b4 iff e SJoins X,Y,G ) );

:: deftheorem Def31 defines .edgesDBetween GLIB_000:def_31_:_
 for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesDBetween (X,Y) iff for e being set holds
( e in b4 iff e DSJoins X,Y,G ) );

scheme :: GLIB_000:sch 1
FinGraphOrderInd{ P1[ finite _Graph] } :
 for G being finite _Graph holds P1[G]
provided
A1: for G being finite _Graph st G .order() = 1 holds
P1[G] and
A2: for k being non empty Nat st ( for Gk being finite _Graph st Gk .order() = k holds
P1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
P1[Gk1]
proofend;

scheme :: GLIB_000:sch 2
FinGraphSizeInd{ P1[ finite _Graph] } :
 for G being finite _Graph holds P1[G]
provided
A1: for G being finite _Graph st G .size() = 0 holds
P1[G] and
A2: for k being Element of NAT st ( for Gk being finite _Graph st Gk .size() = k holds
P1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .size() = k + 1 holds
P1[Gk1]
proofend;

definition
let G be _Graph;
mode Subgraph of G ->  _Graph means :Def32: :: GLIB_000:def 32
( the_Vertices_of it c= the_Vertices_of G &amp; the_Edges_of it c= the_Edges_of G &amp; ( for e being set st e in the_Edges_of it holds
( (the_Source_of it) . e = (the_Source_of G) . e &amp; (the_Target_of it) . e = (the_Target_of G) . e ) ) );
existence
 ex b1 being _Graph st
( the_Vertices_of b1 c= the_Vertices_of G &amp; the_Edges_of b1 c= the_Edges_of G &amp; ( for e being set st e in the_Edges_of b1 holds
( (the_Source_of b1) . e = (the_Source_of G) . e &amp; (the_Target_of b1) . e = (the_Target_of G) . e ) ) )
proofend;
end;

:: deftheorem Def32 defines Subgraph GLIB_000:def_32_:_
 for G, b2 being _Graph holds
( b2 is Subgraph of G iff ( the_Vertices_of b2 c= the_Vertices_of G &amp; the_Edges_of b2 c= the_Edges_of G &amp; ( for e being set st e in the_Edges_of b2 holds
( (the_Source_of b2) . e = (the_Source_of G) . e &amp; (the_Target_of b2) . e = (the_Target_of G) . e ) ) ) );

definition
let G1 be _Graph;
let G2 be Subgraph of G1;
:: original:the_Vertices_of
redefine func the_Vertices_of G2 ->  non empty Subset of (the_Vertices_of G1);
coherence
 the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by Def32;
:: original:the_Edges_of
redefine func the_Edges_of G2 ->  Subset of (the_Edges_of G1);
coherence
 the_Edges_of G2 is Subset of (the_Edges_of G1) by Def32;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple for Subgraph of G;
existence
 ex b1 being Subgraph of G st
( b1 is trivial &amp; b1 is simple )
proofend;
end;

Lm4:  for G being _Graph holds G is Subgraph of G
proofend;

Lm5:  for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
e Joins x,y,G1
proofend;

registration
let G be finite _Graph;
cluster  ->  finite for Subgraph of G;
coherence
 for b1 being Subgraph of G holds b1 is finite
proofend;
end;

registration
let G be loopless _Graph;
cluster  ->  loopless for Subgraph of G;
coherence
 for b1 being Subgraph of G holds b1 is loopless
proofend;
end;

registration
let G be trivial _Graph;
cluster  ->  trivial for Subgraph of G;
coherence
 for b1 being Subgraph of G holds b1 is trivial
proofend;
end;

registration
let G be non-multi _Graph;
cluster  ->  non-multi for Subgraph of G;
coherence
 for b1 being Subgraph of G holds b1 is non-multi
proofend;
end;

definition
let G1 be _Graph;
let G2 be Subgraph of G1;
attrG2 is spanning  means :Def33: :: GLIB_000:def 33
 the_Vertices_of G2 = the_Vertices_of G1;
end;

:: deftheorem Def33 defines spanning GLIB_000:def_33_:_
 for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 is spanning iff the_Vertices_of G2 = the_Vertices_of G1 );

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] spanning for Subgraph of G;
existence
 ex b1 being Subgraph of G st b1 is spanning
proofend;
end;

definition
let G1, G2 be _Graph;
predG1 == G2 means :Def34: :: GLIB_000:def 34
( the_Vertices_of G1 = the_Vertices_of G2 &amp; the_Edges_of G1 = the_Edges_of G2 &amp; the_Source_of G1 = the_Source_of G2 &amp; the_Target_of G1 = the_Target_of G2 );
reflexivity
 for G1 being _Graph holds
( the_Vertices_of G1 = the_Vertices_of G1 &amp; the_Edges_of G1 = the_Edges_of G1 &amp; the_Source_of G1 = the_Source_of G1 &amp; the_Target_of G1 = the_Target_of G1 ) ;
symmetry
 for G1, G2 being _Graph st the_Vertices_of G1 = the_Vertices_of G2 &amp; the_Edges_of G1 = the_Edges_of G2 &amp; the_Source_of G1 = the_Source_of G2 &amp; the_Target_of G1 = the_Target_of G2 holds
( the_Vertices_of G2 = the_Vertices_of G1 &amp; the_Edges_of G2 = the_Edges_of G1 &amp; the_Source_of G2 = the_Source_of G1 &amp; the_Target_of G2 = the_Target_of G1 ) ;
end;

:: deftheorem Def34 defines == GLIB_000:def_34_:_
 for G1, G2 being _Graph holds
( G1 == G2 iff ( the_Vertices_of G1 = the_Vertices_of G2 &amp; the_Edges_of G1 = the_Edges_of G2 &amp; the_Source_of G1 = the_Source_of G2 &amp; the_Target_of G1 = the_Target_of G2 ) );

notation
let G1, G2 be _Graph;
antonym G1 != G2 for G1 == G2;
end;

definition
let G1, G2 be _Graph;
predG1 c= G2 means :Def35: :: GLIB_000:def 35
G1 is Subgraph of G2;
reflexivity
 for G1 being _Graph holds G1 is Subgraph of G1 by Lm4;
end;

:: deftheorem Def35 defines c= GLIB_000:def_35_:_
 for G1, G2 being _Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );

definition
let G1, G2 be _Graph;
predG1 c< G2 means :Def36: :: GLIB_000:def 36
( G1 c= G2 &amp; G1 != G2 );
irreflexivity
 for G1 being _Graph holds
( not G1 c= G1 or not G1 != G1 ) ;
end;

:: deftheorem Def36 defines c< GLIB_000:def_36_:_
 for G1, G2 being _Graph holds
( G1 c< G2 iff ( G1 c= G2 &amp; G1 != G2 ) );

definition
let G be _Graph;
let V, E be set ;
mode inducedSubgraph of G,V,E ->  Subgraph of G means :Def37: :: GLIB_000:def 37
( the_Vertices_of it = V &amp; the_Edges_of it = E ) if ( V is non empty Subset of (the_Vertices_of G) &amp; E c= G .edgesBetween V )
otherwise it == G;
existence
 ( ( V is non empty Subset of (the_Vertices_of G) &amp; E c= G .edgesBetween V implies ex b1 being Subgraph of G st
( the_Vertices_of b1 = V &amp; the_Edges_of b1 = E ) ) &amp; ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b1 being Subgraph of G st b1 == G ) )
proofend;
consistency
 for b1 being Subgraph of G holds verum ;
end;

:: deftheorem Def37 defines inducedSubgraph GLIB_000:def_37_:_
 for G being _Graph
for V, E being set
for b4 being Subgraph of G holds
( ( V is non empty Subset of (the_Vertices_of G) &amp; E c= G .edgesBetween V implies ( b4 is inducedSubgraph of G,V,E iff ( the_Vertices_of b4 = V &amp; the_Edges_of b4 = E ) ) ) &amp; ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b4 is inducedSubgraph of G,V,E iff b4 == G ) ) );

definition
let G be _Graph;
let V be set ;
mode inducedSubgraph of G,V is inducedSubgraph of G,V,G .edgesBetween V;
end;

registration
let G be _Graph;
let V be non empty finite Subset of (the_Vertices_of G);
let E be finite Subset of (G .edgesBetween V);
cluster  ->  finite for inducedSubgraph of G,V,E;
coherence
 for b1 being inducedSubgraph of G,V,E holds b1 is finite
proofend;
end;

registration
let G be _Graph;
let v be Element of the_Vertices_of G;
let E be Subset of (G .edgesBetween {v});
cluster  ->  trivial for inducedSubgraph of G,{v},E;
coherence
 for b1 being inducedSubgraph of G,{v},E holds b1 is trivial
proofend;
end;

registration
let G be _Graph;
let v be Element of the_Vertices_of G;
cluster  ->  finite trivial for inducedSubgraph of G,{v}, {} ;
coherence
 for b1 being inducedSubgraph of G,{v}, {} holds
( b1 is finite &amp; b1 is trivial )
proofend;
end;

registration
let G be _Graph;
let V be non empty Subset of (the_Vertices_of G);
cluster  ->  simple for inducedSubgraph of G,V, {} ;
coherence
 for b1 being inducedSubgraph of G,V, {} holds b1 is simple
proofend;
end;

Lm6:  for G being _Graph
for e, X being set holds
( ( e in the_Edges_of G &amp; (the_Source_of G) . e in X &amp; (the_Target_of G) . e in X ) iff e in G .edgesBetween X )
proofend;

Lm7:  for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)
proofend;

registration
let G be _Graph;
let E be Subset of (the_Edges_of G);
cluster  ->  spanning for inducedSubgraph of G, the_Vertices_of G,E;
coherence
 for b1 being inducedSubgraph of G, the_Vertices_of G,E holds b1 is spanning
proofend;
end;

registration
let G be _Graph;
cluster  ->  spanning for inducedSubgraph of G, the_Vertices_of G, {} ;
coherence
 for b1 being inducedSubgraph of G, the_Vertices_of G, {} holds b1 is spanning
proofend;
end;

definition
let G be _Graph;
let v be set ;
mode removeVertex of G,v is inducedSubgraph of G,((the_Vertices_of G) \ {v});
end;

definition
let G be _Graph;
let V be set ;
mode removeVertices of G,V is inducedSubgraph of G,((the_Vertices_of G) \ V);
end;

definition
let G be _Graph;
let e be set ;
mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
end;

definition
let G be _Graph;
let E be set ;
mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
end;

registration
let G be _Graph;
let e be set ;
cluster  ->  spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
coherence
 for b1 being removeEdge of G,e holds b1 is spanning ;
end;

registration
let G be _Graph;
let E be set ;
cluster  ->  spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
coherence
 for b1 being removeEdges of G,E holds b1 is spanning ;
end;

definition
let G be _Graph;
mode Vertex of G is Element of the_Vertices_of G;
end;

definition
let G be _Graph;
let v be Vertex of G;
funcv .edgesIn()  ->  Subset of (the_Edges_of G) equals :: GLIB_000:def 38
G .edgesInto {v};
coherence
 G .edgesInto {v} is Subset of (the_Edges_of G) ;
funcv .edgesOut()  ->  Subset of (the_Edges_of G) equals :: GLIB_000:def 39
G .edgesOutOf {v};
coherence
 G .edgesOutOf {v} is Subset of (the_Edges_of G) ;
funcv .edgesInOut()  ->  Subset of (the_Edges_of G) equals :: GLIB_000:def 40
G .edgesInOut {v};
coherence
 G .edgesInOut {v} is Subset of (the_Edges_of G) ;
end;

:: deftheorem  defines .edgesIn() GLIB_000:def_38_:_
 for G being _Graph
for v being Vertex of G holds v .edgesIn() = G .edgesInto {v};

:: deftheorem  defines .edgesOut() GLIB_000:def_39_:_
 for G being _Graph
for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v};

:: deftheorem  defines .edgesInOut() GLIB_000:def_40_:_
 for G being _Graph
for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v};

Lm8:  for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesIn() iff ( e in the_Edges_of G &amp; (the_Target_of G) . e = v ) )
proofend;

Lm9:  for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesOut() iff ( e in the_Edges_of G &amp; (the_Source_of G) . e = v ) )
proofend;

definition
let G be _Graph;
let v be Vertex of G;
let e be set ;
funcv .adj e ->  Vertex of G equals :Def41: :: GLIB_000:def 41
(the_Source_of G) . e if ( e in the_Edges_of G &amp; (the_Target_of G) . e = v )
(the_Target_of G) . e if ( e in the_Edges_of G &amp; (the_Source_of G) . e = v &amp; not (the_Target_of G) . e = v )
otherwise v;
coherence
 ( ( e in the_Edges_of G &amp; (the_Target_of G) . e = v implies (the_Source_of G) . e is Vertex of G ) &amp; ( e in the_Edges_of G &amp; (the_Source_of G) . e = v &amp; not (the_Target_of G) . e = v implies (the_Target_of G) . e is Vertex of G ) &amp; ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) &amp; ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v is Vertex of G ) ) by FUNCT_2:5;
consistency
 for b1 being Vertex of G st e in the_Edges_of G &amp; (the_Target_of G) . e = v &amp; e in the_Edges_of G &amp; (the_Source_of G) . e = v &amp; not (the_Target_of G) . e = v holds
( b1 = (the_Source_of G) . e iff b1 = (the_Target_of G) . e ) ;
end;

:: deftheorem Def41 defines .adj GLIB_000:def_41_:_
 for G being _Graph
for v being Vertex of G
for e being set holds
( ( e in the_Edges_of G &amp; (the_Target_of G) . e = v implies v .adj e = (the_Source_of G) . e ) &amp; ( e in the_Edges_of G &amp; (the_Source_of G) . e = v &amp; not (the_Target_of G) . e = v implies v .adj e = (the_Target_of G) . e ) &amp; ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) &amp; ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v .adj e = v ) );

definition
let G be _Graph;
let v be Vertex of G;
funcv .inDegree()  ->  Cardinal equals :: GLIB_000:def 42
 card (v .edgesIn());
coherence
 card (v .edgesIn()) is Cardinal ;
funcv .outDegree()  ->  Cardinal equals :: GLIB_000:def 43
 card (v .edgesOut());
coherence
 card (v .edgesOut()) is Cardinal ;
end;

:: deftheorem  defines .inDegree() GLIB_000:def_42_:_
 for G being _Graph
for v being Vertex of G holds v .inDegree() = card (v .edgesIn());

:: deftheorem  defines .outDegree() GLIB_000:def_43_:_
 for G being _Graph
for v being Vertex of G holds v .outDegree() = card (v .edgesOut());

definition
let G be finite _Graph;
let v be Vertex of G;
:: original:.inDegree()
redefine funcv .inDegree()  ->  Element of NAT ;
coherence
 v .inDegree() is Element of NAT
proofend;
:: original:.outDegree()
redefine funcv .outDegree()  ->  Element of NAT ;
coherence
 v .outDegree() is Element of NAT
proofend;
end;

definition
let G be _Graph;
let v be Vertex of G;
funcv .degree()  ->  Cardinal equals :: GLIB_000:def 44
(v .inDegree()) +` (v .outDegree());
coherence
 (v .inDegree()) +` (v .outDegree()) is Cardinal ;
end;

:: deftheorem  defines .degree() GLIB_000:def_44_:_
 for G being _Graph
for v being Vertex of G holds v .degree() = (v .inDegree()) +` (v .outDegree());

definition
let G be finite _Graph;
let v be Vertex of G;
:: original:.degree()
redefine funcv .degree()  ->  Element of NAT  equals :: GLIB_000:def 45
(v .inDegree()) + (v .outDegree());
correctness
coherence
v .degree() is Element of NAT ;
compatibility
for b1 being Element of NAT holds
( b1 = v .degree() iff b1 = (v .inDegree()) + (v .outDegree()) );
proofend;
end;

:: deftheorem  defines .degree() GLIB_000:def_45_:_
 for G being finite _Graph
for v being Vertex of G holds v .degree() = (v .inDegree()) + (v .outDegree());

definition
let G be _Graph;
let v be Vertex of G;
funcv .inNeighbors()  ->  Subset of (the_Vertices_of G) equals :: GLIB_000:def 46
(the_Source_of G) .: (v .edgesIn());
coherence
 (the_Source_of G) .: (v .edgesIn()) is Subset of (the_Vertices_of G) ;
funcv .outNeighbors()  ->  Subset of (the_Vertices_of G) equals :: GLIB_000:def 47
(the_Target_of G) .: (v .edgesOut());
coherence
 (the_Target_of G) .: (v .edgesOut()) is Subset of (the_Vertices_of G) ;
end;

:: deftheorem  defines .inNeighbors() GLIB_000:def_46_:_
 for G being _Graph
for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn());

:: deftheorem  defines .outNeighbors() GLIB_000:def_47_:_
 for G being _Graph
for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut());

definition
let G be _Graph;
let v be Vertex of G;
funcv .allNeighbors()  ->  Subset of (the_Vertices_of G) equals :: GLIB_000:def 48
(v .inNeighbors()) \/ (v .outNeighbors());
coherence
 (v .inNeighbors()) \/ (v .outNeighbors()) is Subset of (the_Vertices_of G) ;
end;

:: deftheorem  defines .allNeighbors() GLIB_000:def_48_:_
 for G being _Graph
for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors());

definition
let G be _Graph;
let v be Vertex of G;
attrv is isolated  means :Def49: :: GLIB_000:def 49
v .edgesInOut() = {} ;
end;

:: deftheorem Def49 defines isolated GLIB_000:def_49_:_
 for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .edgesInOut() = {} );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is isolated  means :: GLIB_000:def 50
v .degree() = 0 ;
compatibility
 ( v is isolated iff v .degree() = 0 )
proofend;
end;

:: deftheorem  defines isolated GLIB_000:def_50_:_
 for G being finite _Graph
for v being Vertex of G holds
( v is isolated iff v .degree() = 0 );

definition
let G be _Graph;
let v be Vertex of G;
attrv is endvertex  means :Def51: :: GLIB_000:def 51
 ex e being set st
( v .edgesInOut() = {e} &amp; not e Joins v,v,G );
end;

:: deftheorem Def51 defines endvertex GLIB_000:def_51_:_
 for G being _Graph
for v being Vertex of G holds
( v is endvertex iff ex e being set st
( v .edgesInOut() = {e} &amp; not e Joins v,v,G ) );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is endvertex  means :: GLIB_000:def 52
v .degree() = 1;
compatibility
 ( v is endvertex iff v .degree() = 1 )
proofend;
end;

:: deftheorem  defines endvertex GLIB_000:def_52_:_
 for G being finite _Graph
for v being Vertex of G holds
( v is endvertex iff v .degree() = 1 );

definition
let F be ManySortedSet of NAT ;
attrF is Graph-yielding  means :Def53: :: GLIB_000:def 53
 for n being Nat holds F . n is _Graph;
attrF is halting  means :Def54: :: GLIB_000:def 54
 ex n being Nat st F . n = F . (n + 1);
end;

:: deftheorem Def53 defines Graph-yielding GLIB_000:def_53_:_
 for F being ManySortedSet of NAT holds
( F is Graph-yielding iff for n being Nat holds F . n is _Graph );

:: deftheorem Def54 defines halting GLIB_000:def_54_:_
 for F being ManySortedSet of NAT holds
( F is halting iff ex n being Nat st F . n = F . (n + 1) );

definition
let F be ManySortedSet of NAT ;
funcF .Lifespan()  ->  Element of NAT  means :: GLIB_000:def 55
( F . it = F . (it + 1) &amp; ( for n being Nat st F . n = F . (n + 1) holds
it <= n ) ) if F is halting
otherwise it = 0 ;
existence
 ( ( F is halting implies ex b1 being Element of NAT st
( F . b1 = F . (b1 + 1) &amp; ( for n being Nat st F . n = F . (n + 1) holds
b1 <= n ) ) ) &amp; ( not F is halting implies ex b1 being Element of NAT st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT holds
( ( F is halting &amp; F . b1 = F . (b1 + 1) &amp; ( for n being Nat st F . n = F . (n + 1) holds
b1 <= n ) &amp; F . b2 = F . (b2 + 1) &amp; ( for n being Nat st F . n = F . (n + 1) holds
b2 <= n ) implies b1 = b2 ) &amp; ( not F is halting &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
consistency
 for b1 being Element of NAT holds verum ;
end;

:: deftheorem  defines .Lifespan() GLIB_000:def_55_:_
 for F being ManySortedSet of NAT
for b2 being Element of NAT holds
( ( F is halting implies ( b2 = F .Lifespan() iff ( F . b2 = F . (b2 + 1) &amp; ( for n being Nat st F . n = F . (n + 1) holds
b2 <= n ) ) ) ) &amp; ( not F is halting implies ( b2 = F .Lifespan() iff b2 = 0 ) ) );

definition
let F be ManySortedSet of NAT ;
funcF .Result()  ->  set  equals :: GLIB_000:def 56
F . (F .Lifespan());
coherence
 F . (F .Lifespan()) is set ;
end;

:: deftheorem  defines .Result() GLIB_000:def_56_:_
 for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding for set ;
existence
 ex b1 being ManySortedSet of NAT st b1 is Graph-yielding
proofend;
end;

definition
mode GraphSeq is Graph-yielding ManySortedSet of NAT ;
end;

registration
let GSq be GraphSeq;
let x be Nat;
clusterGSq . x ->  Relation-like Function-like ;
coherence
 ( GSq . x is Function-like &amp; GSq . x is Relation-like ) by Def53;
end;

registration
let GSq be GraphSeq;
let x be Nat;
clusterGSq . x ->  NAT -defined finite ;
coherence
 ( GSq . x is NAT -defined &amp; GSq . x is finite ) by Def53;
end;

registration
let GSq be GraphSeq;
let x be Nat;
clusterGSq . x ->  [Graph-like] ;
coherence
 GSq . x is [Graph-like] by Def53;
end;

definition
let GSq be GraphSeq;
attrGSq is finite  means :Def57: :: GLIB_000:def 57
 for x being Nat holds GSq . x is finite ;
attrGSq is loopless  means :Def58: :: GLIB_000:def 58
 for x being Nat holds GSq . x is loopless ;
attrGSq is trivial  means :Def59: :: GLIB_000:def 59
 for x being Nat holds GSq . x is trivial ;
attrGSq is non-trivial  means :Def60: :: GLIB_000:def 60
 for x being Nat holds not GSq . x is trivial ;
attrGSq is non-multi  means :Def61: :: GLIB_000:def 61
 for x being Nat holds GSq . x is non-multi ;
attrGSq is non-Dmulti  means :Def62: :: GLIB_000:def 62
 for x being Nat holds GSq . x is non-Dmulti ;
attrGSq is simple  means :Def63: :: GLIB_000:def 63
 for x being Nat holds GSq . x is simple ;
attrGSq is Dsimple  means :Def64: :: GLIB_000:def 64
 for x being Nat holds GSq . x is Dsimple ;
end;

:: deftheorem Def57 defines finite GLIB_000:def_57_:_
 for GSq being GraphSeq holds
( GSq is finite iff for x being Nat holds GSq . x is finite );

:: deftheorem Def58 defines loopless GLIB_000:def_58_:_
 for GSq being GraphSeq holds
( GSq is loopless iff for x being Nat holds GSq . x is loopless );

:: deftheorem Def59 defines trivial GLIB_000:def_59_:_
 for GSq being GraphSeq holds
( GSq is trivial iff for x being Nat holds GSq . x is trivial );

:: deftheorem Def60 defines non-trivial GLIB_000:def_60_:_
 for GSq being GraphSeq holds
( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial );

:: deftheorem Def61 defines non-multi GLIB_000:def_61_:_
 for GSq being GraphSeq holds
( GSq is non-multi iff for x being Nat holds GSq . x is non-multi );

:: deftheorem Def62 defines non-Dmulti GLIB_000:def_62_:_
 for GSq being GraphSeq holds
( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti );

:: deftheorem Def63 defines simple GLIB_000:def_63_:_
 for GSq being GraphSeq holds
( GSq is simple iff for x being Nat holds GSq . x is simple );

:: deftheorem Def64 defines Dsimple GLIB_000:def_64_:_
 for GSq being GraphSeq holds
( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple );

definition
let GSq be GraphSeq;
redefine attr GSq is halting  means :: GLIB_000:def 65
 ex n being Nat st GSq . n = GSq . (n + 1);
compatibility
 ( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) ) by Def54;
end;

:: deftheorem  defines halting GLIB_000:def_65_:_
 for GSq being GraphSeq holds
( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) );

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless trivial non-multi non-Dmulti simple Dsimple for set ;
existence
 ex b1 being GraphSeq st
( b1 is halting &amp; b1 is finite &amp; b1 is loopless &amp; b1 is trivial &amp; b1 is non-multi &amp; b1 is non-Dmulti &amp; b1 is simple &amp; b1 is Dsimple )
proofend;
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless non-trivial non-multi non-Dmulti simple Dsimple for set ;
existence
 ex b1 being GraphSeq st
( b1 is halting &amp; b1 is finite &amp; b1 is loopless &amp; b1 is non-trivial &amp; b1 is non-multi &amp; b1 is non-Dmulti &amp; b1 is simple &amp; b1 is Dsimple )
proofend;
end;

registration
let GSq be finite GraphSeq;
let x be Nat;
clusterGSq . x ->  finite ;
coherence
 GSq . x is finite by Def57;
end;

registration
let GSq be loopless GraphSeq;
let x be Nat;
clusterGSq . x ->  loopless for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is loopless by Def58;
end;

registration
let GSq be trivial GraphSeq;
let x be Nat;
clusterGSq . x ->  trivial for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is trivial by Def59;
end;

registration
let GSq be non-trivial GraphSeq;
let x be Nat;
clusterGSq . x ->  non trivial for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
not b1 is trivial by Def60;
end;

registration
let GSq be non-multi GraphSeq;
let x be Nat;
clusterGSq . x ->  non-multi for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is non-multi by Def61;
end;

registration
let GSq be non-Dmulti GraphSeq;
let x be Nat;
clusterGSq . x ->  non-Dmulti for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is non-Dmulti by Def62;
end;

registration
let GSq be simple GraphSeq;
let x be Nat;
clusterGSq . x ->  simple for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is simple by Def63;
end;

registration
let GSq be Dsimple GraphSeq;
let x be Nat;
clusterGSq . x ->  Dsimple for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . x holds
b1 is Dsimple by Def64;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding non-multi  ->  non-Dmulti for set ;
coherence
 for b1 being GraphSeq st b1 is non-multi holds
b1 is non-Dmulti
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding simple  ->  loopless non-multi for set ;
coherence
 for b1 being GraphSeq st b1 is simple holds
( b1 is loopless &amp; b1 is non-multi )
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless non-multi  ->  simple for set ;
coherence
 for b1 being GraphSeq st b1 is loopless &amp; b1 is non-multi holds
b1 is simple
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless non-Dmulti  ->  Dsimple for set ;
coherence
 for b1 being GraphSeq st b1 is loopless &amp; b1 is non-Dmulti holds
b1 is Dsimple
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding Dsimple  ->  loopless non-Dmulti for set ;
coherence
 for b1 being GraphSeq st b1 is Dsimple holds
( b1 is loopless &amp; b1 is non-Dmulti )
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless trivial  ->  finite for set ;
coherence
 for b1 being GraphSeq st b1 is trivial &amp; b1 is loopless holds
b1 is finite
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding trivial non-Dmulti  ->  finite for set ;
coherence
 for b1 being GraphSeq st b1 is trivial &amp; b1 is non-Dmulti holds
b1 is finite
proofend;
end;

begin

theorem :: GLIB_000:1
( VertexSelector = 1 &amp; EdgeSelector = 2 &amp; SourceSelector = 3 &amp; TargetSelector = 4 ) ;

theorem :: GLIB_000:2
for G being _Graph holds _GraphSelectors c= dom G
proofend;

theorem :: GLIB_000:3
for GS being GraphStruct holds
( the_Vertices_of GS = GS . VertexSelector &amp; the_Edges_of GS = GS . EdgeSelector &amp; the_Source_of GS = GS . SourceSelector &amp; the_Target_of GS = GS . TargetSelector ) ;

theorem :: GLIB_000:4
for G being _Graph holds
( dom (the_Source_of G) = the_Edges_of G &amp; dom (the_Target_of G) = the_Edges_of G &amp; rng (the_Source_of G) c= the_Vertices_of G &amp; rng (the_Target_of G) c= the_Vertices_of G ) by FUNCT_2:def_1;

theorem :: GLIB_000:5
for GS being GraphStruct holds
( GS is [Graph-like] iff ( _GraphSelectors c= dom GS &amp; not the_Vertices_of GS is empty &amp; the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) &amp; the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) by Lm1;

theorem :: GLIB_000:6
for V being non empty set
for E being set
for S, T being Function of E,V holds
( the_Vertices_of (createGraph (V,E,S,T)) = V &amp; the_Edges_of (createGraph (V,E,S,T)) = E &amp; the_Source_of (createGraph (V,E,S,T)) = S &amp; the_Target_of (createGraph (V,E,S,T)) = T ) by FINSEQ_4:76;

theorem Th7: :: GLIB_000:7
for GS being GraphStruct
for x being set
for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}
proofend;

theorem Th8: :: GLIB_000:8
for GS being GraphStruct
for x being set
for n being Nat holds (GS .set (n,x)) . n = x
proofend;

theorem Th9: :: GLIB_000:9
for GS being GraphStruct
for x being set
for n1, n2 being Nat st n1 <> n2 holds
GS . n2 = (GS .set (n1,x)) . n2
proofend;

theorem :: GLIB_000:10
for G being _Graph
for x being set
for n being Nat st not n in _GraphSelectors holds
( the_Vertices_of G = the_Vertices_of (G .set (n,x)) &amp; the_Edges_of G = the_Edges_of (G .set (n,x)) &amp; the_Source_of G = the_Source_of (G .set (n,x)) &amp; the_Target_of G = the_Target_of (G .set (n,x)) &amp; G .set (n,x) is _Graph )
proofend;

theorem :: GLIB_000:11
for GS being GraphStruct
for x being set holds
( the_Vertices_of (GS .set (VertexSelector,x)) = x &amp; the_Edges_of (GS .set (EdgeSelector,x)) = x &amp; the_Source_of (GS .set (SourceSelector,x)) = x &amp; the_Target_of (GS .set (TargetSelector,x)) = x ) by Th8;

theorem :: GLIB_000:12
for GS being GraphStruct
for x, y being set
for n1, n2 being Nat st n1 <> n2 holds
( n1 in dom ((GS .set (n1,x)) .set (n2,y)) &amp; n2 in dom ((GS .set (n1,x)) .set (n2,y)) &amp; ((GS .set (n1,x)) .set (n2,y)) . n1 = x &amp; ((GS .set (n1,x)) .set (n2,y)) . n2 = y )
proofend;

theorem :: GLIB_000:13
for G being _Graph
for e, x, y being set st e Joins x,y,G holds
( x in the_Vertices_of G &amp; y in the_Vertices_of G )
proofend;

theorem :: GLIB_000:14
for G being _Graph
for e, x, y being set st e Joins x,y,G holds
e Joins y,x,G
proofend;

theorem :: GLIB_000:15
for G being _Graph
for e, x1, y1, x2, y2 being set st e Joins x1,y1,G &amp; e Joins x2,y2,G &amp; not ( x1 = x2 &amp; y1 = y2 ) holds
( x1 = y2 &amp; y1 = x2 )
proofend;

theorem :: GLIB_000:16
for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) by Lm2;

theorem :: GLIB_000:17
for G being _Graph
for e, x, y, X, Y being set st e Joins x,y,G &amp; ( ( x in X &amp; y in Y ) or ( x in Y &amp; y in X ) ) holds
e SJoins X,Y,G
proofend;

theorem :: GLIB_000:18
for G being _Graph holds
( G is loopless iff for v, e being set holds not e Joins v,v,G )
proofend;

theorem :: GLIB_000:19
for G being finite loopless _Graph
for v being Vertex of G holds v .degree() = card (v .edgesInOut())
proofend;

theorem :: GLIB_000:20
for G being non trivial _Graph
for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty
proofend;

theorem :: GLIB_000:21
for G being non trivial _Graph ex v1, v2 being Vertex of G st v1 <> v2
proofend;

theorem Th22: :: GLIB_000:22
for G being trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v}
proofend;

theorem :: GLIB_000:23
for G being loopless trivial _Graph holds the_Edges_of G = {}
proofend;

theorem :: GLIB_000:24
for G being _Graph st the_Edges_of G = {} holds
G is simple
proofend;

theorem :: GLIB_000:25
for G being finite _Graph holds G .order() >= 1
proofend;

theorem :: GLIB_000:26
for G being finite _Graph holds
( G .order() = 1 iff G is trivial ) by Def19;

theorem :: GLIB_000:27
for G being finite _Graph holds
( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )
proofend;

theorem Th28: :: GLIB_000:28
for G being _Graph
for e, X being set holds
( ( e in the_Edges_of G &amp; ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X )
proofend;

theorem :: GLIB_000:29
for G being _Graph
for X being set holds
( G .edgesInto X c= G .edgesInOut X &amp; G .edgesOutOf X c= G .edgesInOut X )
proofend;

theorem :: GLIB_000:30
for G being _Graph holds the_Edges_of G = G .edgesInOut (the_Vertices_of G)
proofend;

theorem :: GLIB_000:31
for G being _Graph
for e, X being set holds
( ( e in the_Edges_of G &amp; (the_Source_of G) . e in X &amp; (the_Target_of G) . e in X ) iff e in G .edgesBetween X ) by Lm6;

theorem :: GLIB_000:32
for G being _Graph
for x, X, y, e being set st x in X &amp; y in X &amp; e Joins x,y,G holds
e in G .edgesBetween X
proofend;

theorem :: GLIB_000:33
for G being _Graph
for X being set holds G .edgesBetween X c= G .edgesInOut X
proofend;

theorem Th34: :: GLIB_000:34
for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)
proofend;

theorem Th35: :: GLIB_000:35
for G being _Graph
for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X)
proofend;

theorem :: GLIB_000:36
for G being _Graph
for X, Y being set st X c= Y holds
G .edgesBetween X c= G .edgesBetween Y
proofend;

theorem :: GLIB_000:37
for G being _Graph
for X1, X2, Y1, Y2 being set st X1 c= X2 &amp; Y1 c= Y2 holds
G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)
proofend;

theorem :: GLIB_000:38
for G being _Graph
for X1, X2, Y1, Y2 being set st X1 c= X2 &amp; Y1 c= Y2 holds
G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)
proofend;

theorem :: GLIB_000:39
for G being _Graph
for v being Vertex of G holds
( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) &amp; v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) )
proofend;

theorem :: GLIB_000:40
for G being _Graph holds G is Subgraph of G by Lm4;

theorem Th41: :: GLIB_000:41
for G1, G2 being _Graph holds
( G1 is Subgraph of G2 &amp; G2 is Subgraph of G1 iff ( the_Vertices_of G1 = the_Vertices_of G2 &amp; the_Edges_of G1 = the_Edges_of G2 &amp; the_Source_of G1 = the_Source_of G2 &amp; the_Target_of G1 = the_Target_of G2 ) )
proofend;

theorem :: GLIB_000:42
for G1 being _Graph
for G2 being Subgraph of G1
for x being set holds
( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) &amp; ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) ;

theorem Th43: :: GLIB_000:43
for G1 being _Graph
for G2 being Subgraph of G1
for G3 being Subgraph of G2 holds G3 is Subgraph of G1
proofend;

theorem Th44: :: GLIB_000:44
for G being _Graph
for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 &amp; the_Edges_of G1 c= the_Edges_of G2 holds
G1 is Subgraph of G2
proofend;

theorem Th45: :: GLIB_000:45
for G1 being _Graph
for G2 being Subgraph of G1 holds
( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) &amp; the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) )
proofend;

theorem :: GLIB_000:46
for G being _Graph
for V1, V2, E1, E2 being set
for G1 being inducedSubgraph of G,V1,E1
for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 &amp; E2 c= E1 &amp; V2 is non empty Subset of (the_Vertices_of G) &amp; E2 c= G .edgesBetween V2 holds
G2 is Subgraph of G1
proofend;

theorem Th47: :: GLIB_000:47
for G1 being non trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} &amp; the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )
proofend;

theorem :: GLIB_000:48
for G1 being finite non trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v holds
( (G2 .order()) + 1 = G1 .order() &amp; (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )
proofend;

theorem Th49: :: GLIB_000:49
for G1 being _Graph
for V being set
for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ V &amp; the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) )
proofend;

theorem :: GLIB_000:50
for G1 being finite _Graph
for V being Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds
( (G2 .order()) + (card V) = G1 .order() &amp; (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() )
proofend;

theorem Th51: :: GLIB_000:51
for G1 being _Graph
for e being set
for G2 being removeEdge of G1,e holds
( the_Vertices_of G2 = the_Vertices_of G1 &amp; the_Edges_of G2 = (the_Edges_of G1) \ {e} )
proofend;

theorem :: GLIB_000:52
for G1 being finite _Graph
for e being set
for G2 being removeEdge of G1,e holds
( G1 .order() = G2 .order() &amp; ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )
proofend;

theorem Th53: :: GLIB_000:53
for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E holds
( the_Vertices_of G2 = the_Vertices_of G1 &amp; the_Edges_of G2 = (the_Edges_of G1) \ E )
proofend;

theorem :: GLIB_000:54
for G1 being finite _Graph
for E being set
for G2 being removeEdges of G1,E holds G1 .order() = G2 .order() by Th53;

theorem :: GLIB_000:55
for G1 being finite _Graph
for E being Subset of (the_Edges_of G1)
for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()
proofend;

theorem :: GLIB_000:56
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesIn() iff ( e in the_Edges_of G &amp; (the_Target_of G) . e = v ) ) by Lm8;

theorem :: GLIB_000:57
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesIn() iff ex x being set st e DJoins x,v,G )
proofend;

theorem :: GLIB_000:58
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesOut() iff ( e in the_Edges_of G &amp; (the_Source_of G) . e = v ) ) by Lm9;

theorem :: GLIB_000:59
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )
proofend;

theorem :: GLIB_000:60
for G being _Graph
for v being Vertex of G holds v .edgesInOut() = (v .edgesIn()) \/ (v .edgesOut()) ;

theorem Th61: :: GLIB_000:61
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesInOut() iff ( e in the_Edges_of G &amp; ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )
proofend;

theorem Th62: :: GLIB_000:62
for G being _Graph
for e, x being set
for v1 being Vertex of G st e Joins v1,x,G holds
e in v1 .edgesInOut()
proofend;

theorem Th63: :: GLIB_000:63
for G being _Graph
for e being set
for v1, v2 being Vertex of G holds
( not e Joins v1,v2,G or ( e in v1 .edgesIn() &amp; e in v2 .edgesOut() ) or ( e in v2 .edgesIn() &amp; e in v1 .edgesOut() ) )
proofend;

theorem :: GLIB_000:64
for G being _Graph
for e being set
for v1 being Vertex of G holds
( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )
proofend;

theorem :: GLIB_000:65
for G being _Graph
for e, x, y being set
for v being Vertex of G st e in v .edgesInOut() &amp; e Joins x,y,G &amp; not v = x holds
v = y
proofend;

theorem :: GLIB_000:66
for G being _Graph
for e being set
for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( v1 .adj e = v2 &amp; v2 .adj e = v1 )
proofend;

theorem :: GLIB_000:67
for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesInOut() iff e Joins v,v .adj e,G )
proofend;

theorem :: GLIB_000:68
for G being finite _Graph
for e being set
for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( 1 <= v1 .degree() &amp; 1 <= v2 .degree() )
proofend;

theorem Th69: :: GLIB_000:69
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G )
proofend;

theorem Th70: :: GLIB_000:70
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G )
proofend;

theorem Th71: :: GLIB_000:71
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being set st e Joins v,x,G )
proofend;

theorem Th72: :: GLIB_000:72
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) &amp; ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) &amp; ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) &amp; ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
proofend;

theorem :: GLIB_000:73
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e in the_Edges_of G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) &amp; ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) &amp; ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) &amp; ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )
proofend;

theorem :: GLIB_000:74
for G1 being _Graph
for G2 being spanning Subgraph of G1
for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1
proofend;

theorem :: GLIB_000:75
for G1 being finite _Graph
for G2 being Subgraph of G1 holds
( G2 .order() <= G1 .order() &amp; G2 .size() <= G1 .size() )
proofend;

theorem :: GLIB_000:76
for G1 being _Graph
for G2 being Subgraph of G1
for X being set holds
( G2 .edgesInto X c= G1 .edgesInto X &amp; G2 .edgesOutOf X c= G1 .edgesOutOf X &amp; G2 .edgesInOut X c= G1 .edgesInOut X &amp; G2 .edgesBetween X c= G1 .edgesBetween X )
proofend;

theorem :: GLIB_000:77
for G1 being _Graph
for G2 being Subgraph of G1
for X, Y being set holds
( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) &amp; G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) )
proofend;

theorem Th78: :: GLIB_000:78
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesIn() c= v1 .edgesIn() &amp; v2 .edgesOut() c= v1 .edgesOut() &amp; v2 .edgesInOut() c= v1 .edgesInOut() )
proofend;

theorem Th79: :: GLIB_000:79
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) &amp; v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) &amp; v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) )
proofend;

theorem :: GLIB_000:80
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2
for e being set st v1 = v2 &amp; e in the_Edges_of G2 holds
v1 .adj e = v2 .adj e
proofend;

theorem :: GLIB_000:81
for G1 being finite _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() <= v1 .inDegree() &amp; v2 .outDegree() <= v1 .outDegree() &amp; v2 .degree() <= v1 .degree() )
proofend;

theorem :: GLIB_000:82
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() c= v1 .inNeighbors() &amp; v2 .outNeighbors() c= v1 .outNeighbors() &amp; v2 .allNeighbors() c= v1 .allNeighbors() )
proofend;

theorem :: GLIB_000:83
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 &amp; v1 is isolated holds
v2 is isolated
proofend;

theorem :: GLIB_000:84
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 &amp; v1 is endvertex &amp; not v2 is endvertex holds
v2 is isolated
proofend;

theorem Th85: :: GLIB_000:85
for G1, G2, G3 being _Graph st G1 == G2 &amp; G2 == G3 holds
G1 == G3
proofend;

theorem Th86: :: GLIB_000:86
for G being _Graph
for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 &amp; the_Edges_of G1 = the_Edges_of G2 holds
G1 == G2
proofend;

theorem Th87: :: GLIB_000:87
for G1, G2 being _Graph holds
( G1 == G2 iff ( G1 is Subgraph of G2 &amp; G2 is Subgraph of G1 ) )
proofend;

theorem Th88: :: GLIB_000:88
for G1, G2 being _Graph
for e, x, y, X, Y being set st G1 == G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) &amp; ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) &amp; ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) &amp; ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) )
proofend;

theorem :: GLIB_000:89
for G1, G2 being _Graph st G1 == G2 holds
( ( G1 is finite implies G2 is finite ) &amp; ( G1 is loopless implies G2 is loopless ) &amp; ( G1 is trivial implies G2 is trivial ) &amp; ( G1 is non-multi implies G2 is non-multi ) &amp; ( G1 is non-Dmulti implies G2 is non-Dmulti ) &amp; ( G1 is simple implies G2 is simple ) &amp; ( G1 is Dsimple implies G2 is Dsimple ) )
proofend;

theorem Th90: :: GLIB_000:90
for G1, G2 being _Graph
for X, Y being set st G1 == G2 holds
( G1 .order() = G2 .order() &amp; G1 .size() = G2 .size() &amp; G1 .edgesInto X = G2 .edgesInto X &amp; G1 .edgesOutOf X = G2 .edgesOutOf X &amp; G1 .edgesInOut X = G2 .edgesInOut X &amp; G1 .edgesBetween X = G2 .edgesBetween X &amp; G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
proofend;

theorem Th91: :: GLIB_000:91
for G1, G2, G3 being _Graph st G1 == G2 &amp; G3 is Subgraph of G1 holds
G3 is Subgraph of G2
proofend;

theorem :: GLIB_000:92
for G1, G2, G3 being _Graph st G1 == G2 &amp; G1 is Subgraph of G3 holds
G2 is Subgraph of G3
proofend;

theorem :: GLIB_000:93
for G being _Graph
for V, E being set
for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2
proofend;

theorem :: GLIB_000:94
for G1 being _Graph
for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2
proofend;

theorem :: GLIB_000:95
for G1, G2 being _Graph
for V, E being set
for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds
G3 is inducedSubgraph of G2,V,E
proofend;

theorem Th96: :: GLIB_000:96
for G1, G2 being _Graph
for e being set
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 &amp; G1 == G2 holds
( v1 .edgesIn() = v2 .edgesIn() &amp; v1 .edgesOut() = v2 .edgesOut() &amp; v1 .edgesInOut() = v2 .edgesInOut() &amp; v1 .adj e = v2 .adj e &amp; v1 .inDegree() = v2 .inDegree() &amp; v1 .outDegree() = v2 .outDegree() &amp; v1 .degree() = v2 .degree() &amp; v1 .inNeighbors() = v2 .inNeighbors() &amp; v1 .outNeighbors() = v2 .outNeighbors() &amp; v1 .allNeighbors() = v2 .allNeighbors() )
proofend;

theorem :: GLIB_000:97
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 &amp; G1 == G2 holds
( ( v1 is isolated implies v2 is isolated ) &amp; ( v1 is endvertex implies v2 is endvertex ) )
proofend;

theorem Th98: :: GLIB_000:98
for G being _Graph
for G1, G2 being Subgraph of G holds
( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )
proofend;

theorem :: GLIB_000:99
for G being _Graph
for G1, G2 being Subgraph of G holds
( not G1 c< G2 or ex v being set st
( v in the_Vertices_of G2 &amp; not v in the_Vertices_of G1 ) or ex e being set st
( e in the_Edges_of G2 &amp; not e in the_Edges_of G1 ) )
proofend;