:: Unification of Graphs and Relations in {M}izar :: by Sebastian Koch :: :: Received May 31, 2020 :: Copyright (c) 2020-2021 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, FUNCT_4, ZFMISC_1, CARD_1, ARYTM_3, XXREAL_0, PBOOLE, GLIB_000, RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD, SCMYCIEL, REWRITE1, GLIB_006, GLIB_007, GLIB_009, GLIB_010, GLIB_012, MCART_1, WAYBEL_0, MOD_4, RELAT_2, GLIB_001, SGRAPH1, GLUNIR00, EQREL_1, GLIB_013; notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, BINOP_1, DOMAIN_1, EQREL_1, FUNCT_3, FUNCT_4, FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, FINSEQ_1, GLIB_000, GLIB_001, GLIB_002, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_012, GLIB_013; constructors DOMAIN_1, FUNCT_4, CHORD, GLIB_002, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_012, COMPUT_1, EQREL_1, GLIB_013; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, PARTFUN1, RELSET_1, GLIB_000, GLIB_002, GLIB_007, GLIB_009, GLIB_008, GLIB_010, XTUPLE_0, GLIB_012, ZFMISC_1, RELAT_2, GLIBPRE0, GLIB_013; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: The Adjacency Relation reserve G for _Graph; definition let G; func VertexDomRel(G) -> Relation of the_Vertices_of G equals :: GLUNIR00:def 1 (the_Source_of G qua Relation)~ * (the_Target_of G); end; theorem :: GLUNIR00:1 for v,w being object holds [v,w] in VertexDomRel(G) iff ex e being object st e DJoins v,w,G; theorem :: GLUNIR00:2 for v,w being object holds [v,w] in (VertexDomRel(G))~ iff ex e being object st e DJoins w,v,G; theorem :: GLUNIR00:3 G is loopless iff VertexDomRel(G) is irreflexive; registration let G be loopless _Graph; cluster VertexDomRel(G) -> irreflexive; end; registration let G be non loopless _Graph; cluster VertexDomRel(G) -> non irreflexive; end; registration let G be non-multi _Graph; cluster VertexDomRel(G) -> antisymmetric; end; registration let G be simple _Graph; cluster VertexDomRel(G) -> asymmetric; end; theorem :: GLUNIR00:4 for G being _Graph st ex e1,e2,x,y being object st e1 DJoins x,y,G & e2 DJoins y,x,G holds VertexDomRel(G) is non asymmetric; registration let G be non non-multi non-Dmulti _Graph; cluster VertexDomRel(G) -> non asymmetric; end; :: means G is then without isolated vertices theorem :: GLUNIR00:5 for G being loopless _Graph st field VertexDomRel(G) = the_Vertices_of G holds for C being Component of G holds C is non _trivial; :: means if G is without isolated vertices theorem :: GLUNIR00:6 for G being _Graph st for C being Component of G holds C is non _trivial holds field VertexDomRel(G) = the_Vertices_of G; theorem :: GLUNIR00:7 for G being non _trivial connected _Graph holds field VertexDomRel(G) = the_Vertices_of G; registration let G be complete _Graph; cluster VertexDomRel(G) -> connected; end; ::registration :: let G be non complete without_isolated_vertices _Graph; :: cluster VertexDomRel(G) -> non connected; :: coherence; ::end; theorem :: GLUNIR00:8 G is edgeless iff VertexDomRel(G) is empty; registration let G be edgeless _Graph; cluster VertexDomRel(G) -> empty; end; registration let G be non edgeless _Graph; cluster VertexDomRel(G) -> non empty; end; theorem :: GLUNIR00:9 G is loopfull iff VertexDomRel(G) is total reflexive; registration let G be loopfull _Graph; cluster VertexDomRel(G) -> reflexive total; end; ::registration :: let G be non loopfull without_isolated_vertices _Graph; :: cluster VertexDomRel(G) -> non reflexive; :: coherence; ::end; registration let G be vertex-finite _Graph; cluster VertexDomRel(G) -> finite; end; theorem :: GLUNIR00:10 card VertexDomRel(G) = card Class DEdgeAdjEqRel(G); theorem :: GLUNIR00:11 card VertexDomRel(G) c= G.size(); theorem :: GLUNIR00:12 for G being non-Dmulti _Graph holds G.size() = card VertexDomRel(G); theorem :: GLUNIR00:13 for v being Vertex of G holds Im(VertexDomRel(G),v) = v.outNeighbors(); theorem :: GLUNIR00:14 for v being Vertex of G holds Coim(VertexDomRel(G),v) = v.inNeighbors(); theorem :: GLUNIR00:15 for H being Subgraph of G holds VertexDomRel(H) c= VertexDomRel(G); theorem :: GLUNIR00:16 for H being removeDParallelEdges of G holds VertexDomRel(H) = VertexDomRel(G); theorem :: GLUNIR00:17 for H being removeLoops of G holds VertexDomRel(H) = VertexDomRel(G) \ id the_Vertices_of G; theorem :: GLUNIR00:18 for H being DSimpleGraph of G holds VertexDomRel(H) = VertexDomRel(G) \ id the_Vertices_of G; theorem :: GLUNIR00:19 for G1, G2 being _Graph st G1 == G2 holds VertexDomRel(G1) = VertexDomRel(G2); theorem :: GLUNIR00:20 for H being reverseEdgeDirections of G holds VertexDomRel(H) = (VertexDomRel(G))~; theorem :: GLUNIR00:21 for V being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G, V holds VertexDomRel(H) = VertexDomRel(G) /\ [: V, V :]; theorem :: GLUNIR00:22 for V being set, H being removeVertices of G, V st V c< the_Vertices_of G holds VertexDomRel(H) = VertexDomRel(G) \ ([: V, the_Vertices_of G :] \/ [: the_Vertices_of G, V :]); theorem :: GLUNIR00:23 for G being non _trivial _Graph, v being Vertex of G for H being removeVertex of G, v holds VertexDomRel(H) = VertexDomRel(G) \ ([: {v}, the_Vertices_of G :] \/ [: the_Vertices_of G, {v} :]); theorem :: GLUNIR00:24 for G being non _trivial _Graph, v being Vertex of G for H being removeVertex of G, v st v is isolated holds VertexDomRel(H) = VertexDomRel(G); theorem :: GLUNIR00:25 for V being set, H being addVertices of G, V holds VertexDomRel(H) = VertexDomRel(G); theorem :: GLUNIR00:26 for v, e, w being object, H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds VertexDomRel(H) = VertexDomRel(G); theorem :: GLUNIR00:27 for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w st not e in the_Edges_of G holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]} ; theorem :: GLUNIR00:28 for v being Vertex of G, e,w being object, H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not w in the_Vertices_of G holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]}; theorem :: GLUNIR00:29 for v,e being object, w being Vertex of G, H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not v in the_Vertices_of G holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]}; :: In their current form addAdjVertexTo/FromAll seem like their definition :: will be changed in the future to allow a more general edge set. :: Therefore the following theorems will not be proven here at the the moment. :: theorem :: for v being object, V being Subset of the_Vertices_of G :: for H being addAdjVertexToAll of G,v,V st not v in the_Vertices_of G :: holds VertexDomRel(H) = VertexDomRel(G) \/ [: {v},V :]; :: :: theorem :: for v being object, V being Subset of the_Vertices_of G :: for H being addAdjVertexFromAll of G,v,V st not v in the_Vertices_of G :: holds VertexDomRel(H) = VertexDomRel(G) \/ [: V,{v} :]; theorem :: GLUNIR00:30 for V being Subset of the_Vertices_of G, H being addLoops of G, V holds VertexDomRel(H) = VertexDomRel(G) \/ id V; theorem :: GLUNIR00:31 for H being DLGraphComplement of G holds VertexDomRel(H) = [: the_Vertices_of G, the_Vertices_of G :] \ VertexDomRel(G); definition let G; func VertexAdjSymRel(G) -> Relation of the_Vertices_of G equals :: GLUNIR00:def 2 VertexDomRel(G) \/ ((VertexDomRel(G))~); end; theorem :: GLUNIR00:32 for v, w being object holds [v,w] in VertexAdjSymRel(G) iff ex e being object st e Joins v,w,G; theorem :: GLUNIR00:33 for v, w being Vertex of G holds [v,w] in VertexAdjSymRel(G) iff v, w are_adjacent; theorem :: GLUNIR00:34 VertexDomRel(G) c= VertexAdjSymRel(G); theorem :: GLUNIR00:35 VertexAdjSymRel(G) = ((the_Source_of G qua Relation)~ * (the_Target_of G)) \/ ((the_Target_of G qua Relation)~ * (the_Source_of G)); registration let G; cluster VertexAdjSymRel(G) -> symmetric; end; theorem :: GLUNIR00:36 G is loopless iff VertexAdjSymRel(G) is irreflexive; registration let G be loopless _Graph; cluster VertexAdjSymRel(G) -> irreflexive; end; registration let G be non loopless _Graph; cluster VertexAdjSymRel(G) -> non irreflexive; end; :: means G is then without isolated vertices theorem :: GLUNIR00:37 for G being loopless _Graph st VertexAdjSymRel(G) is total holds for C being Component of G holds C is non _trivial; :: means if G is without isolated vertices theorem :: GLUNIR00:38 for G being _Graph st for C being Component of G holds C is non _trivial holds VertexAdjSymRel(G) is total; registration let G be non _trivial connected _Graph; cluster VertexAdjSymRel(G) -> total; end; registration let G be complete _Graph; cluster VertexAdjSymRel(G) -> connected; end; :: registration :: let G be non complete without_isolated_vertices _Graph; :: cluster VertexAdjSymRel(G) -> non connected; :: coherence; :: end; theorem :: GLUNIR00:39 G is edgeless iff VertexAdjSymRel(G) is empty; registration let G be edgeless _Graph; cluster VertexAdjSymRel(G) -> empty; end; registration let G be non edgeless _Graph; cluster VertexAdjSymRel(G) -> non empty; end; theorem :: GLUNIR00:40 G is loopfull iff VertexAdjSymRel(G) is total reflexive; registration let G be loopfull _Graph; cluster VertexAdjSymRel(G) -> reflexive total; end; :: registration :: let G be non loopfull without_isolated_vertices _Graph; :: cluster VertexAdjSymRel(G) -> non reflexive; :: coherence; :: end; registration let G be vertex-finite _Graph; cluster VertexAdjSymRel(G) -> finite; end; theorem :: GLUNIR00:41 card Class DEdgeAdjEqRel(G) c= card VertexAdjSymRel(G); theorem :: GLUNIR00:42 card Class EdgeAdjEqRel(G) c= card VertexAdjSymRel(G); theorem :: GLUNIR00:43 for G being non-Dmulti _Graph holds G.size() c= card VertexAdjSymRel(G); theorem :: GLUNIR00:44 for v being Vertex of G holds Im(VertexAdjSymRel(G),v) = v.allNeighbors(); theorem :: GLUNIR00:45 for H being Subgraph of G holds VertexAdjSymRel(H) c= VertexAdjSymRel(G); theorem :: GLUNIR00:46 for H being removeParallelEdges of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G); theorem :: GLUNIR00:47 for H being removeLoops of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ id the_Vertices_of G; theorem :: GLUNIR00:48 for H being SimpleGraph of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ id the_Vertices_of G; theorem :: GLUNIR00:49 for G1, G2 being _Graph st G1 == G2 holds VertexAdjSymRel(G1) = VertexAdjSymRel(G2); theorem :: GLUNIR00:50 for E being set, H being reverseEdgeDirections of G, E holds VertexAdjSymRel(H) = VertexAdjSymRel(G); theorem :: GLUNIR00:51 for V being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G, V holds VertexAdjSymRel(H) = VertexAdjSymRel(G) /\ [: V, V :]; theorem :: GLUNIR00:52 for V being set, H being removeVertices of G, V st V c< the_Vertices_of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ ([: V, the_Vertices_of G :] \/ [: the_Vertices_of G, V :]); theorem :: GLUNIR00:53 for G being non _trivial _Graph, v being Vertex of G for H being removeVertex of G, v holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ ([: {v}, the_Vertices_of G :] \/ [: the_Vertices_of G, {v} :]); theorem :: GLUNIR00:54 for G being non _trivial _Graph, v being Vertex of G for H being removeVertex of G, v st v is isolated holds VertexAdjSymRel(H) = VertexAdjSymRel(G); theorem :: GLUNIR00:55 for V being set, H being addVertices of G, V holds VertexAdjSymRel(H) = VertexAdjSymRel(G); theorem :: GLUNIR00:56 for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w st v,w are_adjacent holds VertexAdjSymRel(H) = VertexAdjSymRel(G); theorem :: GLUNIR00:57 for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w st not e in the_Edges_of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]}; theorem :: GLUNIR00:58 for v being Vertex of G, e,w being object, H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not w in the_Vertices_of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]}; theorem :: GLUNIR00:59 for v,e being object, w being Vertex of G, H being addAdjVertex of G,v,e,w st not e in the_Edges_of G & not v in the_Vertices_of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]}; theorem :: GLUNIR00:60 for v being object, V being Subset of the_Vertices_of G for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ [: {v},V :] \/ [: V,{v} :]; theorem :: GLUNIR00:61 for V being Subset of the_Vertices_of G, H being addLoops of G, V holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ id V; theorem :: GLUNIR00:62 for H being LGraphComplement of G holds VertexAdjSymRel(H) = [: the_Vertices_of G, the_Vertices_of G :] \ VertexAdjSymRel(G); begin :: Create non-Dmulti Graphs from Relations reserve V for non empty set, E for Relation of V; definition let V, E; func createGraph(V,E) -> _Graph equals :: GLUNIR00:def 3 createGraph(V, E, pr1(V,V) | E, pr2(V,V) | E); end; registration let V, E; cluster the_Edges_of createGraph(V,E) -> Relation-like; end; theorem :: GLUNIR00:63 for v,w being object holds [v,w] in E iff [v,w] DJoins v,w,createGraph(V,E); theorem :: GLUNIR00:64 for e,v,w being object st e DJoins v,w,createGraph(V,E) holds e = [v,w]; theorem :: GLUNIR00:65 VertexDomRel(createGraph(V,E)) = E; registration let V, E; reduce VertexDomRel createGraph(V,E) to E; end; registration let V, E; cluster createGraph(V,E) -> plain non-Dmulti; end; theorem :: GLUNIR00:66 V is trivial iff createGraph(V,E) is _trivial; registration let V be trivial non empty set; let E be Relation of V; cluster createGraph(V,E) -> _trivial; end; registration let V be non trivial set; let E be Relation of V; cluster createGraph(V,E) -> non _trivial; end; theorem :: GLUNIR00:67 E is irreflexive iff createGraph(V,E) is loopless; registration let V; let E be irreflexive Relation of V; cluster createGraph(V,E) -> loopless; end; registration let V; let E be non irreflexive Relation of V; cluster createGraph(V,E) -> non loopless; end; theorem :: GLUNIR00:68 E is antisymmetric iff createGraph(V,E) is non-multi; registration let V; let E be antisymmetric Relation of V; cluster createGraph(V,E) -> non-multi; end; registration let V be non trivial set; let E be non antisymmetric Relation of V; cluster createGraph(V,E) -> non non-multi; end; registration let V; let E be asymmetric Relation of V; cluster createGraph(V,E) -> simple; end; theorem :: GLUNIR00:69 createGraph(V,E) is complete implies E is connected; registration let V be non trivial set; let E be non connected Relation of V; cluster createGraph(V,E) -> non complete; end; theorem :: GLUNIR00:70 E is empty iff createGraph(V,E) is edgeless; registration let V; let E be empty Relation of V; cluster createGraph(V,E) -> edgeless; end; registration let V; let E be non empty Relation of V; cluster createGraph(V,E) -> non edgeless; end; theorem :: GLUNIR00:71 E is total reflexive iff createGraph(V,E) is loopfull; registration let V; let E be total reflexive Relation of V; cluster createGraph(V,E) -> loopfull; end; registration let V; let E be non total Relation of V; cluster createGraph(V,E) -> non loopfull; end; registration let V be finite non empty set, E be Relation of V; cluster createGraph(V,E) -> finite; end; registration let V; let E be finite Relation of V; cluster createGraph(V,E) -> edge-finite; end; theorem :: GLUNIR00:72 for v being Vertex of createGraph(V,E) holds Im(E,v) = v.outNeighbors(); theorem :: GLUNIR00:73 for v being Vertex of createGraph(V,E) holds Coim(E,v) = v.inNeighbors(); theorem :: GLUNIR00:74 for X being set holds E|X = createGraph(V,E).edgesOutOf(X); theorem :: GLUNIR00:75 for Y being set holds Y|`E = createGraph(V,E).edgesInto(Y); theorem :: GLUNIR00:76 for X,Y being set holds Y|`E|X = createGraph(V,E).edgesDBetween(X,Y); theorem :: GLUNIR00:77 for X,Y being set holds Y|`E|X \/ X|`E|Y = createGraph(V,E).edgesBetween(X,Y); theorem :: GLUNIR00:78 for v being Vertex of createGraph(V,E) holds E|{v} = v.edgesOut(); theorem :: GLUNIR00:79 for v being Vertex of createGraph(V,E) holds {v}|`E = v.edgesIn(); theorem :: GLUNIR00:80 for X being set holds E|X \/ X|`E = createGraph(V,E).edgesInOut(X); theorem :: GLUNIR00:81 dom E = rng the_Source_of createGraph(V,E); theorem :: GLUNIR00:82 rng E = rng the_Target_of createGraph(V,E); theorem :: GLUNIR00:83 for v being Vertex of createGraph(V,E) holds v is isolated iff not v in field E; theorem :: GLUNIR00:84 E is symmetric iff VertexAdjSymRel(createGraph(V,E)) = E; theorem :: GLUNIR00:85 for V1 being non empty set, V2 being non empty Subset of V1 for E1 being (Relation of V1), E2 being Relation of V2 st E2 c= E1 holds createGraph(V2,E2) is inducedSubgraph of createGraph(V1,E1),V2,E2; theorem :: GLUNIR00:86 for G being non-Dmulti _Graph ex F being PGraphMapping of G, createGraph(the_Vertices_of G,VertexDomRel(G)) st F is Disomorphism & F_V = id the_Vertices_of G & for e being object st e in the_Edges_of G holds F_E.e = [(the_Source_of G).e,(the_Target_of G).e]; theorem :: GLUNIR00:87 for G being non-Dmulti _Graph holds createGraph(the_Vertices_of G,VertexDomRel(G)) is G-Disomorphic; :: Using the isomorphism predicate from WELLORD1:def 8 we could :: also write something like the graphs created from isomorphic relations :: are Disomorphic. However, since the relations can only capture edges :: the number of isolated vertices in both graphs may differ, depending :: the underlying sets V1 and V2 of which E1 and E2 are relations of. :: Therefore, such a theorem is better written after functors :: changing RelStrs to _Graphs are introduced in a later article. begin :: create non-multi Graphs from symmetric Relations reserve E for symmetric Relation of V; definition let V, E; mode GraphFromSymRel of V, E is removeParallelEdges of createGraph(V,E); end; reserve G for GraphFromSymRel of V, E; theorem :: GLUNIR00:88 for v,w being object holds [v,w] in E iff [v,w] DJoins v,w,G or [w,v] DJoins w,v,G; theorem :: GLUNIR00:89 for v, w being Vertex of G holds [v,w] in E iff v,w are_adjacent; registration let V, E; cluster -> non-multi for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:90 the_Edges_of G c= E; theorem :: GLUNIR00:91 for G1, G2 being GraphFromSymRel of V, E holds the_Vertices_of G1 = the_Vertices_of G2; theorem :: GLUNIR00:92 for G1, G2 being GraphFromSymRel of V, E holds G2 is G1-isomorphic; theorem :: GLUNIR00:93 V is trivial iff G is _trivial; registration let V be trivial non empty set; let E be symmetric Relation of V; cluster -> _trivial for GraphFromSymRel of V, E; end; registration let V be non trivial set; let E be symmetric Relation of V; cluster -> non _trivial for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:94 E is irreflexive iff G is loopless; registration let V; let E be symmetric irreflexive Relation of V; cluster -> loopless for GraphFromSymRel of V, E; end; registration let V; let E be symmetric non irreflexive Relation of V; cluster -> non loopless for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:95 G is complete implies E is connected; registration let V be non trivial set; let E be symmetric non connected Relation of V; cluster -> non complete for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:96 E is empty iff G is edgeless; registration let V; let E be empty Relation of V; cluster -> edgeless for GraphFromSymRel of V, E; end; registration let V; let E be symmetric non empty Relation of V; cluster -> non edgeless for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:97 E is total reflexive iff G is loopfull; registration let V; let E be total reflexive symmetric Relation of V; cluster -> loopfull for GraphFromSymRel of V, E; end; registration let V; let E be symmetric non total Relation of V; cluster -> non loopfull for GraphFromSymRel of V, E; end; registration let V be finite non empty set, E be symmetric Relation of V; cluster -> finite for GraphFromSymRel of V, E; end; theorem :: GLUNIR00:98 for v being Vertex of G holds Im(E,v) = v.allNeighbors(); theorem :: GLUNIR00:99 for X being set holds G.edgesInOut(X) c= (E|X) \/ (X|`E); theorem :: GLUNIR00:100 for X, Y being set holds G.edgesBetween(X,Y) c= Y|`E|X \/ X|`E|Y; ::theorem :: for v being Vertex of G holds card(E|{v}) = card(v.edgesInOut()); theorem :: GLUNIR00:101 for v being Vertex of G holds v.edgesOut() c= E|{v}; theorem :: GLUNIR00:102 for v being Vertex of G holds v.edgesIn() c= {v}|`E; theorem :: GLUNIR00:103 for v being Vertex of G holds v is isolated iff not v in field E; theorem :: GLUNIR00:104 for G being GraphFromSymRel of V, E holds VertexAdjSymRel(G) = E; theorem :: GLUNIR00:105 for V1 being non empty set, V2 being non empty Subset of V1 for E1 being symmetric Relation of V1 for E2 being symmetric Relation of V2 for G1 being GraphFromSymRel of V1, E1, G2 being GraphFromSymRel of V2, E2 st E2 c= E1 ex F being PGraphMapping of G2, G1 st F is weak_SG-embedding & F_V = id V2 & for v,w being object st [v,w] in the_Edges_of G2 holds F_E.[v,w] = [v,w] or F_E.[v,w] = [w,v]; theorem :: GLUNIR00:106 for G1 being non-multi _Graph for G2 being GraphFromSymRel of the_Vertices_of G1, VertexAdjSymRel(G1) ex F being PGraphMapping of G1, G2 st F is isomorphism & F_V = id the_Vertices_of G1 & for e being object st e in the_Edges_of G1 holds F_E.e = [(the_Source_of G1).e,(the_Target_of G1).e] or F_E.e = [(the_Target_of G1).e,(the_Source_of G1).e]; theorem :: GLUNIR00:107 for G1 being non-multi _Graph for G2 being GraphFromSymRel of the_Vertices_of G1, VertexAdjSymRel(G1) holds G2 is G1-isomorphic;