:: Graphs :: by Krzysztof Hryniewiecki :: :: Received December 5, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition attrc1 is strict ; struct MultiGraphStruct -> 2-sorted ; aggrMultiGraphStruct(# carrier, carrier', Source, Target #) -> MultiGraphStruct ; sel Source c1 -> Function of the carrier' of c1, the carrier of c1; sel Target c1 -> Function of the carrier' of c1, the carrier of c1; end; definition let G be MultiGraphStruct ; mode Vertex of G is Element of G; mode Edge of G is Element of the carrier' of G; end; registration cluster non empty non void strict for MultiGraphStruct ; existence ex b1 being MultiGraphStruct st ( b1 is strict & not b1 is empty & not b1 is void ) proofend; end; definition mode Graph is non empty MultiGraphStruct ; end; :: from CAT_1, 2008.07.02, A.T. definition let C be MultiGraphStruct ; let f be Edge of C; func dom f -> Vertex of C equals :Def1: :: GRAPH_1:def 1 the Source of C . f if ( not C is void & not C is empty ) otherwise the Vertex of C; coherence ( ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) ) proofend; consistency for b1 being Vertex of C holds verum ; func cod f -> Vertex of C equals :Def2: :: GRAPH_1:def 2 the Target of C . f if ( not C is void & not C is empty ) otherwise the Vertex of C; correctness coherence ( ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) ); consistency for b1 being Vertex of C holds verum; proofend; end; :: deftheorem Def1 defines dom GRAPH_1:def_1_:_ for C being MultiGraphStruct for f being Edge of C holds ( ( not C is void & not C is empty implies dom f = the Source of C . f ) & ( ( C is void or C is empty ) implies dom f = the Vertex of C ) ); :: deftheorem Def2 defines cod GRAPH_1:def_2_:_ for C being MultiGraphStruct for f being Edge of C holds ( ( not C is void & not C is empty implies cod f = the Target of C . f ) & ( ( C is void or C is empty ) implies cod f = the Vertex of C ) ); definition let C be non empty non void MultiGraphStruct ; let f be Edge of C; :: original:dom redefine func dom f -> Vertex of C equals :: GRAPH_1:def 3 the Source of C . f; compatibility for b1 being Vertex of C holds ( b1 = dom f iff b1 = the Source of C . f ) by Def1; coherence dom f is Vertex of C ; :: original:cod redefine func cod f -> Vertex of C equals :: GRAPH_1:def 4 the Target of C . f; compatibility for b1 being Vertex of C holds ( b1 = cod f iff b1 = the Target of C . f ) by Def2; coherence cod f is Vertex of C ; end; :: deftheorem defines dom GRAPH_1:def_3_:_ for C being non empty non void MultiGraphStruct for f being Edge of C holds dom f = the Source of C . f; :: deftheorem defines cod GRAPH_1:def_4_:_ for C being non empty non void MultiGraphStruct for f being Edge of C holds cod f = the Target of C . f; definition let G1, G2 be Graph; assume that A1: the Source of G1 tolerates the Source of G2 and A2: the Target of G1 tolerates the Target of G2 ; funcG1 \/ G2 -> strict Graph means :Def5: :: GRAPH_1:def 5 ( the carrier of it = the carrier of G1 \/ the carrier of G2 & the carrier' of it = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of it . v = the Source of G1 . v & the Target of it . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of it . v = the Source of G2 . v & the Target of it . v = the Target of G2 . v ) ) ); existence ex b1 being strict Graph st ( the carrier of b1 = the carrier of G1 \/ the carrier of G2 & the carrier' of b1 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of b1 . v = the Source of G1 . v & the Target of b1 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of b1 . v = the Source of G2 . v & the Target of b1 . v = the Target of G2 . v ) ) ) proofend; uniqueness for b1, b2 being strict Graph st the carrier of b1 = the carrier of G1 \/ the carrier of G2 & the carrier' of b1 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of b1 . v = the Source of G1 . v & the Target of b1 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of b1 . v = the Source of G2 . v & the Target of b1 . v = the Target of G2 . v ) ) & the carrier of b2 = the carrier of G1 \/ the carrier of G2 & the carrier' of b2 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of b2 . v = the Source of G1 . v & the Target of b2 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of b2 . v = the Source of G2 . v & the Target of b2 . v = the Target of G2 . v ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines \/ GRAPH_1:def_5_:_ for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds for b3 being strict Graph holds ( b3 = G1 \/ G2 iff ( the carrier of b3 = the carrier of G1 \/ the carrier of G2 & the carrier' of b3 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of b3 . v = the Source of G1 . v & the Target of b3 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of b3 . v = the Source of G2 . v & the Target of b3 . v = the Target of G2 . v ) ) ) ); definition let G, G1, G2 be Graph; predG is_sum_of G1,G2 means :Def6: :: GRAPH_1:def 6 ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ); end; :: deftheorem Def6 defines is_sum_of GRAPH_1:def_6_:_ for G, G1, G2 being Graph holds ( G is_sum_of G1,G2 iff ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ) ); definition let IT be Graph; attrIT is oriented means :Def7: :: GRAPH_1:def 7 for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds x = y; attrIT is non-multi means :Def8: :: GRAPH_1:def 8 for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds x = y; attrIT is simple means :Def9: :: GRAPH_1:def 9 for x being set holds ( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ); attrIT is connected means :Def10: :: GRAPH_1:def 10 for G1, G2 being Graph holds ( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ); end; :: deftheorem Def7 defines oriented GRAPH_1:def_7_:_ for IT being Graph holds ( IT is oriented iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds x = y ); :: deftheorem Def8 defines non-multi GRAPH_1:def_8_:_ for IT being Graph holds ( IT is non-multi iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds x = y ); :: deftheorem Def9 defines simple GRAPH_1:def_9_:_ for IT being Graph holds ( IT is simple iff for x being set holds ( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ) ); :: deftheorem Def10 defines connected GRAPH_1:def_10_:_ for IT being Graph holds ( IT is connected iff for G1, G2 being Graph holds ( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ) ); definition let IT be MultiGraphStruct ; attrIT is finite means :Def11: :: GRAPH_1:def 11 ( the carrier of IT is finite & the carrier' of IT is finite ); end; :: deftheorem Def11 defines finite GRAPH_1:def_11_:_ for IT being MultiGraphStruct holds ( IT is finite iff ( the carrier of IT is finite & the carrier' of IT is finite ) ); registration cluster finite for MultiGraphStruct ; existence ex b1 being MultiGraphStruct st b1 is finite proofend; cluster non empty feasible oriented non-multi simple connected finite for MultiGraphStruct ; existence ex b1 being Graph st ( b1 is finite & b1 is non-multi & b1 is oriented & b1 is simple & b1 is connected ) proofend; end; registration let G be finite MultiGraphStruct ; cluster the carrier of G -> finite ; coherence the carrier of G is finite by Def11; cluster the carrier' of G -> finite ; coherence the carrier' of G is finite by Def11; end; definition let G be Graph; let x, y be Element of the carrier of G; let v be set ; predv joins x,y means :: GRAPH_1:def 12 ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ); end; :: deftheorem defines joins GRAPH_1:def_12_:_ for G being Graph for x, y being Element of the carrier of G for v being set holds ( v joins x,y iff ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ) ); definition let G be Graph; let x, y be Element of the carrier of G; predx,y are_incident means :: GRAPH_1:def 13 ex v being set st ( v in the carrier' of G & v joins x,y ); end; :: deftheorem defines are_incident GRAPH_1:def_13_:_ for G being Graph for x, y being Element of the carrier of G holds ( x,y are_incident iff ex v being set st ( v in the carrier' of G & v joins x,y ) ); definition let G be Graph; mode Chain of G -> FinSequence means :Def14: :: GRAPH_1:def 14 ( ( for n being Element of NAT st 1 <= n & n <= len it holds it . n in the carrier' of G ) & ex p being FinSequence st ( len p = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len it holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & it . n joins x9,y9 ) ) ) ); existence ex b1 being FinSequence st ( ( for n being Element of NAT st 1 <= n & n <= len b1 holds b1 . n in the carrier' of G ) & ex p being FinSequence st ( len p = (len b1) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b1 holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & b1 . n joins x9,y9 ) ) ) ) proofend; end; :: deftheorem Def14 defines Chain GRAPH_1:def_14_:_ for G being Graph for b2 being FinSequence holds ( b2 is Chain of G iff ( ( for n being Element of NAT st 1 <= n & n <= len b2 holds b2 . n in the carrier' of G ) & ex p being FinSequence st ( len p = (len b2) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b2 holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & b2 . n joins x9,y9 ) ) ) ) ); Lm1: for G being Graph holds {} is Chain of G proofend; definition let G be Graph; :: original:Chain redefine mode Chain of G -> FinSequence of the carrier' of G; coherence for b1 being Chain of G holds b1 is FinSequence of the carrier' of G proofend; end; definition let G be Graph; let IT be Chain of G; attrIT is oriented means :: GRAPH_1:def 15 for n being Element of NAT st 1 <= n & n < len IT holds the Source of G . (IT . (n + 1)) = the Target of G . (IT . n); end; :: deftheorem defines oriented GRAPH_1:def_15_:_ for G being Graph for IT being Chain of G holds ( IT is oriented iff for n being Element of NAT st 1 <= n & n < len IT holds the Source of G . (IT . (n + 1)) = the Target of G . (IT . n) ); registration let G be Graph; cluster Relation-like NAT -defined the carrier' of G -valued Function-like empty finite FinSequence-like FinSubsequence-like for Chain of G; existence ex b1 being Chain of G st b1 is empty proofend; end; registration let G be Graph; cluster empty -> oriented for Chain of G; coherence for b1 being Chain of G st b1 is empty holds b1 is oriented proofend; end; definition let G be Graph; let IT be Chain of G; :: original:one-to-one redefine attrIT is one-to-one means :: GRAPH_1:def 16 for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m; compatibility ( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m ) proofend; end; :: deftheorem defines one-to-one GRAPH_1:def_16_:_ for G being Graph for IT being Chain of G holds ( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m ); definition let G be Graph; mode Path of G is V7() Chain of G; end; definition let G be Graph; mode OrientedPath of G is V7() oriented Chain of G; end; definition let G be Graph; let IT be Path of G; attrIT is cyclic means :: GRAPH_1:def 17 ex p being FinSequence st ( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ); end; :: deftheorem defines cyclic GRAPH_1:def_17_:_ for G being Graph for IT being Path of G holds ( IT is cyclic iff ex p being FinSequence st ( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ) ); registration let G be Graph; cluster one-to-one empty -> cyclic for Chain of G; coherence for b1 being Path of G st b1 is empty holds b1 is cyclic proofend; end; definition let G be Graph; mode Cycle of G is cyclic Path of G; end; definition let G be Graph; mode OrientedCycle of G is cyclic OrientedPath of G; end; definition let G be Graph; mode Subgraph of G -> Graph means :Def18: :: GRAPH_1:def 18 ( the carrier of it c= the carrier of G & the carrier' of it c= the carrier' of G & ( for v being set st v in the carrier' of it holds ( the Source of it . v = the Source of G . v & the Target of it . v = the Target of G . v & the Source of G . v in the carrier of it & the Target of G . v in the carrier of it ) ) ); existence ex b1 being Graph st ( the carrier of b1 c= the carrier of G & the carrier' of b1 c= the carrier' of G & ( for v being set st v in the carrier' of b1 holds ( the Source of b1 . v = the Source of G . v & the Target of b1 . v = the Target of G . v & the Source of G . v in the carrier of b1 & the Target of G . v in the carrier of b1 ) ) ) proofend; end; :: deftheorem Def18 defines Subgraph GRAPH_1:def_18_:_ for G, b2 being Graph holds ( b2 is Subgraph of G iff ( the carrier of b2 c= the carrier of G & the carrier' of b2 c= the carrier' of G & ( for v being set st v in the carrier' of b2 holds ( the Source of b2 . v = the Source of G . v & the Target of b2 . v = the Target of G . v & the Source of G . v in the carrier of b2 & the Target of G . v in the carrier of b2 ) ) ) ); registration let G be Graph; cluster non empty feasible strict for Subgraph of G; existence ex b1 being Subgraph of G st b1 is strict proofend; end; definition let G be finite Graph; func VerticesCount G -> Element of NAT means :: GRAPH_1:def 19 ex B being finite set st ( B = the carrier of G & it = card B ); existence ex b1 being Element of NAT ex B being finite set st ( B = the carrier of G & b1 = card B ) proofend; uniqueness for b1, b2 being Element of NAT st ex B being finite set st ( B = the carrier of G & b1 = card B ) & ex B being finite set st ( B = the carrier of G & b2 = card B ) holds b1 = b2 ; func EdgesCount G -> Element of NAT means :: GRAPH_1:def 20 ex B being finite set st ( B = the carrier' of G & it = card B ); existence ex b1 being Element of NAT ex B being finite set st ( B = the carrier' of G & b1 = card B ) proofend; uniqueness for b1, b2 being Element of NAT st ex B being finite set st ( B = the carrier' of G & b1 = card B ) & ex B being finite set st ( B = the carrier' of G & b2 = card B ) holds b1 = b2 ; end; :: deftheorem defines VerticesCount GRAPH_1:def_19_:_ for G being finite Graph for b2 being Element of NAT holds ( b2 = VerticesCount G iff ex B being finite set st ( B = the carrier of G & b2 = card B ) ); :: deftheorem defines EdgesCount GRAPH_1:def_20_:_ for G being finite Graph for b2 being Element of NAT holds ( b2 = EdgesCount G iff ex B being finite set st ( B = the carrier' of G & b2 = card B ) ); definition let G be finite Graph; let x be Vertex of G; func EdgesIn x -> Element of NAT means :: GRAPH_1:def 21 ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & it = card X ); existence ex b1 being Element of NAT ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b1 = card X ) proofend; uniqueness for b1, b2 being Element of NAT st ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b1 = card X ) & ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b2 = card X ) holds b1 = b2 proofend; func EdgesOut x -> Element of NAT means :: GRAPH_1:def 22 ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & it = card X ); existence ex b1 being Element of NAT ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b1 = card X ) proofend; uniqueness for b1, b2 being Element of NAT st ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b1 = card X ) & ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b2 = card X ) holds b1 = b2 proofend; end; :: deftheorem defines EdgesIn GRAPH_1:def_21_:_ for G being finite Graph for x being Vertex of G for b3 being Element of NAT holds ( b3 = EdgesIn x iff ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b3 = card X ) ); :: deftheorem defines EdgesOut GRAPH_1:def_22_:_ for G being finite Graph for x being Vertex of G for b3 being Element of NAT holds ( b3 = EdgesOut x iff ex X being finite set st ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b3 = card X ) ); definition let G be finite Graph; let x be Vertex of G; func Degree x -> Element of NAT equals :: GRAPH_1:def 23 (EdgesIn x) + (EdgesOut x); correctness coherence (EdgesIn x) + (EdgesOut x) is Element of NAT ; ; end; :: deftheorem defines Degree GRAPH_1:def_23_:_ for G being finite Graph for x being Vertex of G holds Degree x = (EdgesIn x) + (EdgesOut x); Lm2: for n being Element of NAT for G being Graph for p being Chain of G holds p | (Seg n) is Chain of G proofend; Lm3: for G being Graph for H1, H2 being strict Subgraph of G st the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 holds H1 = H2 proofend; definition let G1, G2 be Graph; predG1 c= G2 means :Def24: :: GRAPH_1:def 24 G1 is Subgraph of G2; reflexivity for G1 being Graph holds G1 is Subgraph of G1 proofend; end; :: deftheorem Def24 defines c= GRAPH_1:def_24_:_ for G1, G2 being Graph holds ( G1 c= G2 iff G1 is Subgraph of G2 ); Lm4: for G being Graph for H being Subgraph of G holds ( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) ) proofend; definition let G be Graph; func bool G -> set means :Def25: :: GRAPH_1:def 25 for x being set holds ( x in it iff x is strict Subgraph of G ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict Subgraph of G ) proofend; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict Subgraph of G ) ) & ( for x being set holds ( x in b2 iff x is strict Subgraph of G ) ) holds b1 = b2 proofend; end; :: deftheorem Def25 defines bool GRAPH_1:def_25_:_ for G being Graph for b2 being set holds ( b2 = bool G iff for x being set holds ( x in b2 iff x is strict Subgraph of G ) ); scheme :: GRAPH_1:sch 1 GraphSeparation{ F1() -> Graph, P1[ set ] } : ex X being set st for x being set holds ( x in X iff ( x is strict Subgraph of F1() & P1[x] ) ) proofend; :: Properties of graphs :: theorem :: GRAPH_1:1 for G being Graph holds ( dom the Source of G = the carrier' of G & dom the Target of G = the carrier' of G ) by FUNCT_2:def_1; theorem :: GRAPH_1:2 for G being Graph for x being Vertex of G holds x in the carrier of G ; theorem :: GRAPH_1:3 for G being Graph for v being set st v in the carrier' of G holds ( the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5; :: Chain :: theorem :: GRAPH_1:4 for n being Element of NAT for G being Graph for p being Chain of G holds p | (Seg n) is Chain of G by Lm2; :: Sum of two graphs :: theorem Th5: :: GRAPH_1:5 for G1, G being Graph st G1 c= G holds ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G ) proofend; theorem :: GRAPH_1:6 for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds ( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 ) proofend; theorem Th7: :: GRAPH_1:7 for G being strict Graph holds G = G \/ G proofend; theorem Th8: :: GRAPH_1:8 for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds G1 \/ G2 = G2 \/ G1 proofend; theorem Th9: :: GRAPH_1:9 for G1, G2, G3 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G3 & the Target of G1 tolerates the Target of G3 & the Source of G2 tolerates the Source of G3 & the Target of G2 tolerates the Target of G3 holds (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) proofend; theorem Th10: :: GRAPH_1:10 for G, G1, G2 being Graph st G is_sum_of G1,G2 holds G is_sum_of G2,G1 proofend; theorem :: GRAPH_1:11 for G being strict Graph holds G is_sum_of G,G proofend; :: Graphs' inclusion :: theorem Th12: :: GRAPH_1:12 for G1, G2 being Graph st ex G being Graph st ( G1 c= G & G2 c= G ) holds G1 \/ G2 = G2 \/ G1 proofend; theorem :: GRAPH_1:13 for G1, G2, G3 being Graph st ex G being Graph st ( G1 c= G & G2 c= G & G3 c= G ) holds (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) proofend; theorem :: GRAPH_1:14 for G being Graph holds {} is Chain of G by Lm1; theorem :: GRAPH_1:15 for G being Graph for H1, H2 being strict Subgraph of G st the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 holds H1 = H2 by Lm3; theorem Th16: :: GRAPH_1:16 for G1, G2 being strict Graph st G1 c= G2 & G2 c= G1 holds G1 = G2 proofend; theorem Th17: :: GRAPH_1:17 for G1, G2, G3 being Graph st G1 c= G2 & G2 c= G3 holds G1 c= G3 proofend; theorem Th18: :: GRAPH_1:18 for G, G1, G2 being Graph st G is_sum_of G1,G2 holds ( G1 c= G & G2 c= G ) proofend; theorem Th19: :: GRAPH_1:19 for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) proofend; theorem Th20: :: GRAPH_1:20 for G1, G2 being Graph st ex G being Graph st ( G1 c= G & G2 c= G ) holds ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) proofend; theorem Th21: :: GRAPH_1:21 for G1, G3, G2, G being Graph st G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 holds G c= G3 proofend; theorem Th22: :: GRAPH_1:22 for G1, G, G2 being Graph st G1 c= G & G2 c= G holds G1 \/ G2 c= G proofend; theorem :: GRAPH_1:23 for G1, G2 being strict Graph st G1 c= G2 holds ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) proofend; theorem Th24: :: GRAPH_1:24 for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) holds G1 c= G2 proofend; theorem :: GRAPH_1:25 for G1 being Graph for G being oriented Graph st G1 c= G holds G1 is oriented proofend; theorem :: GRAPH_1:26 for G1 being Graph for G being non-multi Graph st G1 c= G holds G1 is non-multi proofend; theorem :: GRAPH_1:27 for G1 being Graph for G being simple Graph st G1 c= G holds G1 is simple proofend; :: Set of all subgraphs :: theorem :: GRAPH_1:28 for G being Graph for G1 being strict Graph holds ( G1 in bool G iff G1 c= G ) proofend; theorem Th29: :: GRAPH_1:29 for G being strict Graph holds G in bool G proofend; theorem :: GRAPH_1:30 for G2 being Graph for G1 being strict Graph holds ( G1 c= G2 iff bool G1 c= bool G2 ) proofend; theorem :: GRAPH_1:31 for G being strict Graph holds {G} c= bool G proofend; theorem :: GRAPH_1:32 for G1, G2 being strict Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & bool (G1 \/ G2) c= (bool G1) \/ (bool G2) & not G1 c= G2 holds G2 c= G1 proofend; theorem :: GRAPH_1:33 for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds (bool G1) \/ (bool G2) c= bool (G1 \/ G2) proofend; theorem :: GRAPH_1:34 for G1, G, G2 being Graph st G1 in bool G & G2 in bool G holds G1 \/ G2 in bool G proofend;