:: GRAPH_1 semantic presentation 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 ) proof ( not MultiGraphStruct(# 1,1,op1,op1 #) is empty & not MultiGraphStruct(# 1,1,op1,op1 #) is void ) ; hence ex b1 being MultiGraphStruct st ( b1 is strict & not b1 is empty & not b1 is void ) ; ::_thesis: verum end; end; definition mode Graph is non empty MultiGraphStruct ; end; 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 ) ) proof thus ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) ::_thesis: ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) proof assume ( not C is void & not C is empty ) ; ::_thesis: the Source of C . f is Vertex of C then reconsider C = C as non empty non void MultiGraphStruct ; reconsider f = f as Edge of C ; the Source of C . f is Vertex of C ; hence the Source of C . f is Vertex of C ; ::_thesis: verum end; thus ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) ; ::_thesis: verum end; 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; proof thus ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) ::_thesis: ( ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) & ( for b1 being Vertex of C holds verum ) ) proof assume ( not C is void & not C is empty ) ; ::_thesis: the Target of C . f is Vertex of C then reconsider C = C as non empty non void MultiGraphStruct ; reconsider f = f as Edge of C ; the Target of C . f is Vertex of C ; hence the Target of C . f is Vertex of C ; ::_thesis: verum end; thus ( ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) & ( for b1 being Vertex of C holds verum ) ) ; ::_thesis: verum end; 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 ) ) ) proof set V = the carrier of G1 \/ the carrier of G2; set E = the carrier' of G1 \/ the carrier' of G2; ex S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) st ( ( for v being set st v in the carrier' of G1 holds S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds S . v = the Source of G2 . v ) ) proof defpred S1[ set , set ] means ( ( \$1 in the carrier' of G1 implies \$2 = the Source of G1 . \$1 ) & ( \$1 in the carrier' of G2 implies \$2 = the Source of G2 . \$1 ) ); A3: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) assume A4: x in the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) A5: ( x in the carrier' of G1 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) proof assume A6: x in the carrier' of G1 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) take y = the Source of G1 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) y in the carrier of G1 by A6, FUNCT_2:5; hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y] thus ( x in the carrier' of G1 implies y = the Source of G1 . x ) ; ::_thesis: ( x in the carrier' of G2 implies y = the Source of G2 . x ) assume x in the carrier' of G2 ; ::_thesis: y = the Source of G2 . x then A7: x in the carrier' of G1 /\ the carrier' of G2 by A6, XBOOLE_0:def_4; dom the Source of G1 = the carrier' of G1 by FUNCT_2:def_1; then x in (dom the Source of G1) /\ (dom the Source of G2) by A7, FUNCT_2:def_1; hence y = the Source of G2 . x by A1, PARTFUN1:def_4; ::_thesis: verum end; ( not x in the carrier' of G1 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) proof assume A8: not x in the carrier' of G1 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) then A9: x in the carrier' of G2 by A4, XBOOLE_0:def_3; take y = the Source of G2 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) y in the carrier of G2 by A9, FUNCT_2:5; hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y] thus S1[x,y] by A8; ::_thesis: verum end; hence ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A5; ::_thesis: verum end; consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that A10: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds S1[x,S . x] from FUNCT_2:sch_1(A3); take S ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds S . v = the Source of G2 . v ) ) thus for v being set st v in the carrier' of G1 holds S . v = the Source of G1 . v ::_thesis: for v being set st v in the carrier' of G2 holds S . v = the Source of G2 . v proof let v be set ; ::_thesis: ( v in the carrier' of G1 implies S . v = the Source of G1 . v ) assume A11: v in the carrier' of G1 ; ::_thesis: S . v = the Source of G1 . v then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3; hence S . v = the Source of G1 . v by A10, A11; ::_thesis: verum end; let v be set ; ::_thesis: ( v in the carrier' of G2 implies S . v = the Source of G2 . v ) assume A12: v in the carrier' of G2 ; ::_thesis: S . v = the Source of G2 . v then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3; hence S . v = the Source of G2 . v by A10, A12; ::_thesis: verum end; then consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that A13: for v being set st v in the carrier' of G1 holds S . v = the Source of G1 . v and A14: for v being set st v in the carrier' of G2 holds S . v = the Source of G2 . v ; ex T being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) st ( ( for v being set st v in the carrier' of G1 holds T . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds T . v = the Target of G2 . v ) ) proof defpred S1[ set , set ] means ( ( \$1 in the carrier' of G1 implies \$2 = the Target of G1 . \$1 ) & ( \$1 in the carrier' of G2 implies \$2 = the Target of G2 . \$1 ) ); A15: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) assume A16: x in the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) A17: ( x in the carrier' of G1 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) proof assume A18: x in the carrier' of G1 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) take y = the Target of G1 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) y in the carrier of G1 by A18, FUNCT_2:5; hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y] thus ( x in the carrier' of G1 implies y = the Target of G1 . x ) ; ::_thesis: ( x in the carrier' of G2 implies y = the Target of G2 . x ) assume x in the carrier' of G2 ; ::_thesis: y = the Target of G2 . x then A19: x in the carrier' of G1 /\ the carrier' of G2 by A18, XBOOLE_0:def_4; dom the Target of G1 = the carrier' of G1 by FUNCT_2:def_1; then x in (dom the Target of G1) /\ (dom the Target of G2) by A19, FUNCT_2:def_1; hence y = the Target of G2 . x by A2, PARTFUN1:def_4; ::_thesis: verum end; ( not x in the carrier' of G1 implies ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) ) proof assume A20: not x in the carrier' of G1 ; ::_thesis: ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) then A21: x in the carrier' of G2 by A16, XBOOLE_0:def_3; take y = the Target of G2 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) y in the carrier of G2 by A21, FUNCT_2:5; hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y] thus S1[x,y] by A20; ::_thesis: verum end; hence ex y being set st ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A17; ::_thesis: verum end; consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that A22: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds S1[x,S . x] from FUNCT_2:sch_1(A15); take S ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds S . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds S . v = the Target of G2 . v ) ) thus for v being set st v in the carrier' of G1 holds S . v = the Target of G1 . v ::_thesis: for v being set st v in the carrier' of G2 holds S . v = the Target of G2 . v proof let v be set ; ::_thesis: ( v in the carrier' of G1 implies S . v = the Target of G1 . v ) assume A23: v in the carrier' of G1 ; ::_thesis: S . v = the Target of G1 . v then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3; hence S . v = the Target of G1 . v by A22, A23; ::_thesis: verum end; let v be set ; ::_thesis: ( v in the carrier' of G2 implies S . v = the Target of G2 . v ) assume A24: v in the carrier' of G2 ; ::_thesis: S . v = the Target of G2 . v then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3; hence S . v = the Target of G2 . v by A22, A24; ::_thesis: verum end; then consider T being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that A25: for v being set st v in the carrier' of G1 holds T . v = the Target of G1 . v and A26: for v being set st v in the carrier' of G2 holds T . v = the Target of G2 . v ; reconsider G = MultiGraphStruct(# ( the carrier of G1 \/ the carrier of G2),( the carrier' of G1 \/ the carrier' of G2),S,T #) as strict Graph ; take G ; ::_thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) ) thus the carrier of G = the carrier of G1 \/ the carrier of G2 ; ::_thesis: ( the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) ) thus the carrier' of G = the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) ) thus for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) by A13, A25; ::_thesis: for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) let v be set ; ::_thesis: ( v in the carrier' of G2 implies ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) assume A27: v in the carrier' of G2 ; ::_thesis: ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) hence the Source of G . v = the Source of G2 . v by A14; ::_thesis: the Target of G . v = the Target of G2 . v thus the Target of G . v = the Target of G2 . v by A26, A27; ::_thesis: verum end; 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 proof let G, G9 be strict Graph; ::_thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) & the carrier of G9 = the carrier of G1 \/ the carrier of G2 & the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds ( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds ( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ) implies G = G9 ) assume that A28: the carrier of G = the carrier of G1 \/ the carrier of G2 and A29: the carrier' of G = the carrier' of G1 \/ the carrier' of G2 and A30: for v being set st v in the carrier' of G1 holds ( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) and A31: for v being set st v in the carrier' of G2 holds ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) and A32: the carrier of G9 = the carrier of G1 \/ the carrier of G2 and A33: the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 and A34: for v being set st v in the carrier' of G1 holds ( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) and A35: for v being set st v in the carrier' of G2 holds ( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ; ::_thesis: G = G9 A36: ( dom the Source of G = the carrier' of G & dom the Source of G9 = the carrier' of G ) by A29, A33, FUNCT_2:def_1; A37: ( dom the Target of G = the carrier' of G & dom the Target of G9 = the carrier' of G ) by A29, A33, FUNCT_2:def_1; for x being set st x in the carrier' of G holds the Source of G . x = the Source of G9 . x proof let x be set ; ::_thesis: ( x in the carrier' of G implies the Source of G . x = the Source of G9 . x ) assume A38: x in the carrier' of G ; ::_thesis: the Source of G . x = the Source of G9 . x A39: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_the_Source_of_G_._x_=_the_Source_of_G9_._x_) assume A40: x in the carrier' of G1 ; ::_thesis: the Source of G . x = the Source of G9 . x hence the Source of G . x = the Source of G1 . x by A30 .= the Source of G9 . x by A34, A40 ; ::_thesis: verum end; now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_the_Source_of_G_._x_=_the_Source_of_G9_._x_) assume A41: x in the carrier' of G2 ; ::_thesis: the Source of G . x = the Source of G9 . x hence the Source of G . x = the Source of G2 . x by A31 .= the Source of G9 . x by A35, A41 ; ::_thesis: verum end; hence the Source of G . x = the Source of G9 . x by A29, A38, A39, XBOOLE_0:def_3; ::_thesis: verum end; then A42: the Source of G = the Source of G9 by A36, FUNCT_1:2; for x being set st x in the carrier' of G holds the Target of G . x = the Target of G9 . x proof let x be set ; ::_thesis: ( x in the carrier' of G implies the Target of G . x = the Target of G9 . x ) assume A43: x in the carrier' of G ; ::_thesis: the Target of G . x = the Target of G9 . x A44: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_the_Target_of_G_._x_=_the_Target_of_G9_._x_) assume A45: x in the carrier' of G1 ; ::_thesis: the Target of G . x = the Target of G9 . x hence the Target of G . x = the Target of G1 . x by A30 .= the Target of G9 . x by A34, A45 ; ::_thesis: verum end; now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_the_Target_of_G_._x_=_the_Target_of_G9_._x_) assume A46: x in the carrier' of G2 ; ::_thesis: the Target of G . x = the Target of G9 . x hence the Target of G . x = the Target of G2 . x by A31 .= the Target of G9 . x by A35, A46 ; ::_thesis: verum end; hence the Target of G . x = the Target of G9 . x by A29, A43, A44, XBOOLE_0:def_3; ::_thesis: verum end; hence G = G9 by A28, A29, A32, A33, A37, A42, FUNCT_1:2; ::_thesis: verum end; 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 proof take G = MultiGraphStruct(# 1,1,op1,op1 #); ::_thesis: G is finite thus the carrier of G is finite ; :: according to GRAPH_1:def_11 ::_thesis: the carrier' of G is finite thus the carrier' of G is finite ; ::_thesis: verum end; 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 ) proof set V = {1}; reconsider empty1 = {} as Function of {},{1} by RELSET_1:12; reconsider G = MultiGraphStruct(# {1},{},empty1,empty1 #) as Graph ; take G ; ::_thesis: ( G is finite & G is non-multi & G is oriented & G is simple & G is connected ) thus G is finite by Def11; ::_thesis: ( G is non-multi & G is oriented & G is simple & G is connected ) for x, y being set st x in the carrier' of G & y in the carrier' of G & ( ( the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y ) or ( the Source of G . x = the Target of G . y & the Source of G . y = the Target of G . x ) ) holds x = y ; hence G is non-multi by Def8; ::_thesis: ( G is oriented & G is simple & G is connected ) for x, y being set st x in the carrier' of G & y in the carrier' of G & the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y holds x = y ; hence G is oriented by Def7; ::_thesis: ( G is simple & G is connected ) for x being set holds ( not x in the carrier' of G or not the Source of G . x = the Target of G . x ) ; hence G is simple by Def9; ::_thesis: G is connected for G1, G2 being Graph holds ( not the carrier of G1 misses the carrier of G2 or not G is_sum_of G1,G2 ) proof given G1, G2 being Graph such that A1: the carrier of G1 misses the carrier of G2 and A2: G is_sum_of G1,G2 ; ::_thesis: contradiction A3: the carrier of G1 /\ the carrier of G2 = {} by A1, XBOOLE_0:def_7; A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A2, Def6; G = G1 \/ G2 by A2, Def6; then A5: the carrier of G1 \/ the carrier of G2 = {1} by A4, Def5; set x = the Vertex of G1; ( the Vertex of G1 in the carrier of G1 & the Vertex of G1 in {1} ) by A5, XBOOLE_0:def_3; then A6: 1 in the carrier of G1 by TARSKI:def_1; set y = the Vertex of G2; ( the Vertex of G2 in the carrier of G2 & the Vertex of G2 in {1} ) by A5, XBOOLE_0:def_3; then 1 in the carrier of G2 by TARSKI:def_1; hence contradiction by A3, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence G is connected by Def10; ::_thesis: verum end; 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 ) ) ) ) proof take {} ; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len {} holds {} . n in the carrier' of G ) & ex p being FinSequence st ( len p = (len {}) + 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 {} holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) ) ) thus for n being Element of NAT st 1 <= n & n <= len {} holds {} . n in the carrier' of G by XXREAL_0:2; ::_thesis: ex p being FinSequence st ( len p = (len {}) + 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 {} holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) ) set x = the Vertex of G; A1: the Vertex of G in the carrier of G ; take <* the Vertex of G*> ; ::_thesis: ( len <* the Vertex of G*> = (len {}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) ) thus len <* the Vertex of G*> = (len {}) + 1 by FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) ) thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G ) assume that A2: 1 <= n and A3: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G n <= 1 by A3, FINSEQ_1:39; then n = 1 by A2, XXREAL_0:1; hence <* the Vertex of G*> . n in the carrier of G by A1, FINSEQ_1:40; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) by XXREAL_0:2; ::_thesis: verum end; 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 proof let G be Graph; ::_thesis: {} is Chain of G thus for n being Element of NAT st 1 <= n & n <= len {} holds {} . n in the carrier' of G by XXREAL_0:2; :: according to GRAPH_1:def_14 ::_thesis: ex p being FinSequence st ( len p = (len {}) + 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 {} holds ex x9, y9 being Vertex of G st ( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) ) set x = the Vertex of G; A1: the Vertex of G in the carrier of G ; take <* the Vertex of G*> ; ::_thesis: ( len <* the Vertex of G*> = (len {}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) ) thus len <* the Vertex of G*> = (len {}) + 1 by FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) ) thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G ) assume that A2: 1 <= n and A3: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G n <= 1 by A3, FINSEQ_1:39; then n = 1 by A2, XXREAL_0:1; hence <* the Vertex of G*> . n in the carrier of G by A1, FINSEQ_1:40; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) by XXREAL_0:2; ::_thesis: verum end; 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 proof let c be Chain of G; ::_thesis: c is FinSequence of the carrier' of G rng c c= the carrier' of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in the carrier' of G ) assume y in rng c ; ::_thesis: y in the carrier' of G then consider x being set such that A1: x in dom c and A2: y = c . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A1; ( 1 <= x & x <= len c ) by A1, FINSEQ_3:25; hence y in the carrier' of G by A2, Def14; ::_thesis: verum end; hence c is FinSequence of the carrier' of G by FINSEQ_1:def_4; ::_thesis: verum end; 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 proof {} is Chain of G by Lm1; hence ex b1 being Chain of G st b1 is empty ; ::_thesis: verum end; 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 proof let C be Chain of G; ::_thesis: ( C is empty implies C is oriented ) assume A1: C is empty ; ::_thesis: C is oriented let n be Element of NAT ; :: according to GRAPH_1:def_15 ::_thesis: ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) ) thus ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) ) by A1, CARD_1:27, XXREAL_0:2; ::_thesis: verum end; 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 ) proof thus ( IT is one-to-one implies for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m ) ::_thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m ) implies IT is one-to-one ) proof assume A1: IT is one-to-one ; ::_thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len IT implies IT . n <> IT . m ) assume that A2: 1 <= n and A3: n < m and A4: m <= len IT ; ::_thesis: IT . n <> IT . m A5: n <= len IT by A3, A4, XXREAL_0:2; A6: 1 <= m by A2, A3, XXREAL_0:2; A7: n in dom IT by A2, A5, FINSEQ_3:25; m in dom IT by A4, A6, FINSEQ_3:25; hence IT . n <> IT . m by A1, A3, A7, FUNCT_1:def_4; ::_thesis: verum end; assume A8: for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds IT . n <> IT . m ; ::_thesis: IT is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom IT or not x2 in dom IT or not IT . x1 = IT . x2 or x1 = x2 ) assume that A9: ( x1 in dom IT & x2 in dom IT ) and A10: IT . x1 = IT . x2 ; ::_thesis: x1 = x2 reconsider x9 = x1, y9 = x2 as Element of NAT by A9; A11: ( x9 <= len IT & 1 <= y9 ) by A9, FINSEQ_3:25; A12: ( 1 <= x9 & y9 <= len IT ) by A9, FINSEQ_3:25; percases ( x9 <> y9 or x9 = y9 ) ; supposeA13: x9 <> y9 ; ::_thesis: x1 = x2 now__::_thesis:_x1_=_x2 percases ( x9 < y9 or y9 < x9 ) by A13, XXREAL_0:1; suppose x9 < y9 ; ::_thesis: x1 = x2 hence x1 = x2 by A8, A10, A12; ::_thesis: verum end; suppose y9 < x9 ; ::_thesis: x1 = x2 hence x1 = x2 by A8, A10, A11; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; suppose x9 = y9 ; ::_thesis: x1 = x2 hence x1 = x2 ; ::_thesis: verum end; end; end; 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 proof let p be Path of G; ::_thesis: ( p is empty implies p is cyclic ) assume A1: p is empty ; ::_thesis: p is cyclic set x = the Vertex of G; A2: the Vertex of G in the carrier of G ; take <* the Vertex of G*> ; :: according to GRAPH_1:def_17 ::_thesis: ( len <* the Vertex of G*> = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) ) thus len <* the Vertex of G*> = (len p) + 1 by A1, CARD_1:27, FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) ) thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds <* the Vertex of G*> . n in the carrier of G ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len p holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) ) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G ) assume that A3: 1 <= n and A4: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G n <= 1 by A4, FINSEQ_1:39; then n = 1 by A3, XXREAL_0:1; hence <* the Vertex of G*> . n in the carrier of G by A2, FINSEQ_1:40; ::_thesis: verum end; thus for n being Element of NAT st 1 <= n & n <= len p holds ex x9, y9 being Vertex of G st ( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) by A1, CARD_1:27, XXREAL_0:2; ::_thesis: <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) thus <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) by FINSEQ_1:39; ::_thesis: verum end; 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 ) ) ) proof take G ; ::_thesis: ( the carrier of G c= the carrier of G & the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) ) thus the carrier of G c= the carrier of G ; ::_thesis: ( the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) ) thus the carrier' of G c= the carrier' of G ; ::_thesis: for v being set st v in the carrier' of G holds ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) let v be set ; ::_thesis: ( v in the carrier' of G implies ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) assume v in the carrier' of G ; ::_thesis: ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) hence ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5; ::_thesis: verum end; 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 proof reconsider S = MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) as Graph ; for v being set st v in the carrier' of S holds ( the Source of S . v = the Source of G . v & the Target of S . v = the Target of G . v & the Source of G . v in the carrier of S & the Target of G . v in the carrier of S ) by FUNCT_2:5; then S is Subgraph of G by Def18; hence ex b1 being Subgraph of G st b1 is strict ; ::_thesis: verum end; 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 ) proof set B = the carrier of G; take card the carrier of G ; ::_thesis: ex B being finite set st ( B = the carrier of G & card the carrier of G = card B ) take the carrier of G ; ::_thesis: ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G ) thus ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G ) ; ::_thesis: verum end; 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 ) proof set B = the carrier' of G; take card the carrier' of G ; ::_thesis: ex B being finite set st ( B = the carrier' of G & card the carrier' of G = card B ) take the carrier' of G ; ::_thesis: ( the carrier' of G = the carrier' of G & card the carrier' of G = card the carrier' of G ) thus ( the carrier' of G = the carrier' of G & card the carrier' of G = card the carrier' of G ) ; ::_thesis: verum end; 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 ) proof defpred S1[ set ] means the Target of G . \$1 = x; consider X being set such that A1: for z being set holds ( z in X iff ( z in the carrier' of G & S1[z] ) ) from XBOOLE_0:sch_1(); for z being set st z in X holds z in the carrier' of G by A1; then X c= the carrier' of G by TARSKI:def_3; then reconsider X = X as finite set ; take card X ; ::_thesis: 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 ) ) ) & card X = card X ) take X ; ::_thesis: ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X ) thus ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X ) by A1; ::_thesis: verum end; 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 proof let n1, n2 be Element of NAT ; ::_thesis: ( 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 ) ) ) & n1 = 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 ) ) ) & n2 = card X ) implies n1 = n2 ) assume that A2: 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 ) ) ) & n1 = card X ) and A3: 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 ) ) ) & n2 = card X ) ; ::_thesis: n1 = n2 consider X1 being finite set such that A4: for z being set holds ( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) and A5: n1 = card X1 by A2; consider X2 being finite set such that A6: for z being set holds ( z in X2 iff ( z in the carrier' of G & the Target of G . z = x ) ) and A7: n2 = card X2 by A3; for z being set holds ( z in X1 iff z in X2 ) proof let z be set ; ::_thesis: ( z in X1 iff z in X2 ) ( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) by A4; hence ( z in X1 iff z in X2 ) by A6; ::_thesis: verum end; hence n1 = n2 by A5, A7, TARSKI:1; ::_thesis: verum end; 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 ) proof defpred S1[ set ] means the Source of G . \$1 = x; consider X being set such that A8: for z being set holds ( z in X iff ( z in the carrier' of G & S1[z] ) ) from XBOOLE_0:sch_1(); for z being set st z in X holds z in the carrier' of G by A8; then X c= the carrier' of G by TARSKI:def_3; then reconsider X = X as finite set ; take card X ; ::_thesis: 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 ) ) ) & card X = card X ) take X ; ::_thesis: ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & card X = card X ) thus ( ( for z being set holds ( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & card X = card X ) by A8; ::_thesis: verum end; 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 proof let n1, n2 be Element of NAT ; ::_thesis: ( 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 ) ) ) & n1 = 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 ) ) ) & n2 = card X ) implies n1 = n2 ) assume that A9: 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 ) ) ) & n1 = card X ) and A10: 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 ) ) ) & n2 = card X ) ; ::_thesis: n1 = n2 consider X1 being finite set such that A11: for z being set holds ( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) and A12: n1 = card X1 by A9; consider X2 being finite set such that A13: for z being set holds ( z in X2 iff ( z in the carrier' of G & the Source of G . z = x ) ) and A14: n2 = card X2 by A10; for z being set holds ( z in X1 iff z in X2 ) proof let z be set ; ::_thesis: ( z in X1 iff z in X2 ) ( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) by A11; hence ( z in X1 iff z in X2 ) by A13; ::_thesis: verum end; hence n1 = n2 by A12, A14, TARSKI:1; ::_thesis: verum end; 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 proof let n be Element of NAT ; ::_thesis: for G being Graph for p being Chain of G holds p | (Seg n) is Chain of G let G be Graph; ::_thesis: for p being Chain of G holds p | (Seg n) is Chain of G let p be Chain of G; ::_thesis: p | (Seg n) is Chain of G reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15; A1: for n being Element of NAT st 1 <= n & n <= len q holds q . n in the carrier' of G proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len q implies q . k in the carrier' of G ) assume that A2: 1 <= k and A3: k <= len q ; ::_thesis: q . k in the carrier' of G A4: k in dom q by A2, A3, FINSEQ_3:25; dom q c= dom p by RELAT_1:60; then k <= len p by A4, FINSEQ_3:25; then p . k in the carrier' of G by A2, Def14; hence q . k in the carrier' of G by A4, FUNCT_1:47; ::_thesis: verum end; ex q1 being FinSequence st ( len q1 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q1 holds q1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds ex x9, y9 being Vertex of G st ( x9 = q1 . n & y9 = q1 . (n + 1) & q . n joins x9,y9 ) ) ) proof consider q1 being FinSequence such that A5: len q1 = (len p) + 1 and A6: for n being Element of NAT st 1 <= n & n <= len q1 holds q1 . n in the carrier of G and A7: for n being Element of NAT st 1 <= n & n <= len p holds ex x9, y9 being Vertex of G st ( x9 = q1 . n & y9 = q1 . (n + 1) & p . n joins x9,y9 ) by Def14; reconsider q2 = q1 | (Seg (n + 1)) as FinSequence by FINSEQ_1:15; take q2 ; ::_thesis: ( len q2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q2 holds q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds ex x9, y9 being Vertex of G st ( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) ) thus A8: len q2 = (len q) + 1 ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len q2 holds q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds ex x9, y9 being Vertex of G st ( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) ) proof A9: dom q2 = (dom q1) /\ (Seg (n + 1)) by RELAT_1:61 .= (Seg ((len p) + 1)) /\ (Seg (n + 1)) by A5, FINSEQ_1:def_3 ; A10: dom q = (dom p) /\ (Seg n) by RELAT_1:61 .= (Seg (len p)) /\ (Seg n) by FINSEQ_1:def_3 ; A11: now__::_thesis:_(_(len_p)_+_1_<=_n_+_1_implies_len_q2_=_(len_q)_+_1_) assume A12: (len p) + 1 <= n + 1 ; ::_thesis: len q2 = (len q) + 1 then Seg ((len p) + 1) c= Seg (n + 1) by FINSEQ_1:5; then dom q2 = Seg ((len p) + 1) by A9, XBOOLE_1:28; then A13: len q2 = (len p) + 1 by FINSEQ_1:def_3; len p <= n by A12, XREAL_1:6; then Seg (len p) c= Seg n by FINSEQ_1:5; then dom q = Seg (len p) by A10, XBOOLE_1:28; hence len q2 = (len q) + 1 by A13, FINSEQ_1:def_3; ::_thesis: verum end; now__::_thesis:_(_n_+_1_<=_(len_p)_+_1_implies_len_q2_=_(len_q)_+_1_) assume A14: n + 1 <= (len p) + 1 ; ::_thesis: len q2 = (len q) + 1 then Seg (n + 1) c= Seg ((len p) + 1) by FINSEQ_1:5; then dom q2 = Seg (n + 1) by A9, XBOOLE_1:28; then A15: len q2 = n + 1 by FINSEQ_1:def_3; n <= len p by A14, XREAL_1:6; then Seg n c= Seg (len p) by FINSEQ_1:5; then dom q = Seg n by A10, XBOOLE_1:28; hence len q2 = (len q) + 1 by A15, FINSEQ_1:def_3; ::_thesis: verum end; hence len q2 = (len q) + 1 by A11; ::_thesis: verum end; thus for n being Element of NAT st 1 <= n & n <= len q2 holds q2 . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len q holds ex x9, y9 being Vertex of G st ( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len q2 implies q2 . n in the carrier of G ) assume that A16: 1 <= n and A17: n <= len q2 ; ::_thesis: q2 . n in the carrier of G A18: n in dom q2 by A16, A17, FINSEQ_3:25; dom q2 c= dom q1 by RELAT_1:60; then n <= len q1 by A18, FINSEQ_3:25; then q1 . n in the carrier of G by A6, A16; hence q2 . n in the carrier of G by A18, FUNCT_1:47; ::_thesis: verum end; let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len q implies ex x9, y9 being Vertex of G st ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) ) assume that A19: 1 <= k and A20: k <= len q ; ::_thesis: ex x9, y9 being Vertex of G st ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) A21: k in dom q by A19, A20, FINSEQ_3:25; dom q c= dom p by RELAT_1:60; then k <= len p by A21, FINSEQ_3:25; then consider x9, y9 being Vertex of G such that A22: x9 = q1 . k and A23: y9 = q1 . (k + 1) and A24: p . k joins x9,y9 by A7, A19; take x9 ; ::_thesis: ex y9 being Vertex of G st ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) take y9 ; ::_thesis: ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) len q <= (len q) + 1 by NAT_1:11; then k <= len q2 by A8, A20, XXREAL_0:2; then k in dom q2 by A19, FINSEQ_3:25; hence x9 = q2 . k by A22, FUNCT_1:47; ::_thesis: ( y9 = q2 . (k + 1) & q . k joins x9,y9 ) A25: k + 1 <= len q2 by A8, A20, XREAL_1:7; 1 + 1 <= k + 1 by A19, XREAL_1:7; then 1 <= k + 1 by XXREAL_0:2; then k + 1 in dom q2 by A25, FINSEQ_3:25; hence y9 = q2 . (k + 1) by A23, FUNCT_1:47; ::_thesis: q . k joins x9,y9 thus q . k joins x9,y9 by A21, A24, FUNCT_1:47; ::_thesis: verum end; hence p | (Seg n) is Chain of G by A1, Def14; ::_thesis: verum end; 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 proof let G be Graph; ::_thesis: 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 let H1, H2 be strict Subgraph of G; ::_thesis: ( the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 implies H1 = H2 ) assume that A1: the carrier of H1 = the carrier of H2 and A2: the carrier' of H1 = the carrier' of H2 ; ::_thesis: H1 = H2 A3: ( dom the Source of H1 = the carrier' of H1 & dom the Source of H2 = the carrier' of H2 ) by FUNCT_2:def_1; A4: ( dom the Target of H1 = the carrier' of H1 & dom the Target of H2 = the carrier' of H2 ) by FUNCT_2:def_1; for x being set st x in the carrier' of H1 holds the Source of H1 . x = the Source of H2 . x proof let x be set ; ::_thesis: ( x in the carrier' of H1 implies the Source of H1 . x = the Source of H2 . x ) assume A5: x in the carrier' of H1 ; ::_thesis: the Source of H1 . x = the Source of H2 . x hence the Source of H1 . x = the Source of G . x by Def18 .= the Source of H2 . x by A2, A5, Def18 ; ::_thesis: verum end; then A6: the Source of H1 = the Source of H2 by A2, A3, FUNCT_1:2; for x being set st x in the carrier' of H1 holds the Target of H1 . x = the Target of H2 . x proof let x be set ; ::_thesis: ( x in the carrier' of H1 implies the Target of H1 . x = the Target of H2 . x ) assume A7: x in the carrier' of H1 ; ::_thesis: the Target of H1 . x = the Target of H2 . x hence the Target of H1 . x = the Target of G . x by Def18 .= the Target of H2 . x by A2, A7, Def18 ; ::_thesis: verum end; hence H1 = H2 by A1, A2, A4, A6, FUNCT_1:2; ::_thesis: verum end; 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 proof let G be Graph; ::_thesis: G is Subgraph of G for v being set st v in the carrier' of G holds ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5; hence G is Subgraph of G by Def18; ::_thesis: verum end; 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) ) proof let G be Graph; ::_thesis: 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) ) let H be Subgraph of G; ::_thesis: ( 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) ) set EH = the carrier' of H; set VH = the carrier of H; set EG = the carrier' of G; set VG = the carrier of G; ( the carrier' of H c= the carrier' of G & the carrier of H c= the carrier of G ) by Def18; then ( Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of H, the carrier of H) & PFuncs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) ) by FUNCT_2:72, PARTFUN1:50; then A1: Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) by XBOOLE_1:1; the Source of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8; hence the Source of H in PFuncs ( the carrier' of G, the carrier of G) by A1; ::_thesis: the Target of H in PFuncs ( the carrier' of G, the carrier of G) the Target of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8; hence the Target of H in PFuncs ( the carrier' of G, the carrier of G) by A1; ::_thesis: verum end; 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 ) proof reconsider V = the carrier of G as non empty set ; set E = the carrier' of G; set Prod = [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):]; defpred S1[ set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] ex M being Graph ex v being non empty set ex e being set ex s, t being Function of e,v st ( y = \$1 & v = y `1_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G ); consider X being set such that A1: for x being set holds ( x in X iff ( x in [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] & S1[x] ) ) from XBOOLE_0:sch_1(); defpred S2[ set , set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] ex M being strict Graph ex v being non empty set ex e being set ex s, t being Function of e,v st ( y = \$1 & v = y `1_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G & \$2 = M ); A2: for a, b, c being set st S2[a,b] & S2[a,c] holds b = c ; consider Y being set such that A3: for z being set holds ( z in Y iff ex x being set st ( x in X & S2[x,z] ) ) from TARSKI:sch_1(A2); take Y ; ::_thesis: for x being set holds ( x in Y iff x is strict Subgraph of G ) let x be set ; ::_thesis: ( x in Y iff x is strict Subgraph of G ) thus ( x in Y implies x is strict Subgraph of G ) ::_thesis: ( x is strict Subgraph of G implies x in Y ) proof assume x in Y ; ::_thesis: x is strict Subgraph of G then ex z being set st ( z in X & S2[z,x] ) by A3; hence x is strict Subgraph of G ; ::_thesis: verum end; assume x is strict Subgraph of G ; ::_thesis: x in Y then reconsider H = x as strict Subgraph of G ; ex y being set st ( y in X & S2[y,x] ) proof take y = [ the carrier of H, the carrier' of H, the Source of H, the Target of H]; ::_thesis: ( y in X & S2[y,x] ) A4: ( the carrier of H c= V & the carrier' of H c= the carrier' of G ) by Def18; ( the Source of H in PFuncs ( the carrier' of G,V) & the Target of H in PFuncs ( the carrier' of G,V) ) by Lm4; then reconsider y9 = y as Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] by A4, MCART_1:80; reconsider v = the carrier of H as non empty set ; set e = the carrier' of H; reconsider s = the Source of H as Function of the carrier' of H,v ; reconsider t = the Target of H as Function of the carrier' of H,v ; A5: ( v = y9 `1_4 & the carrier' of H = y9 `2_4 ) by MCART_1:def_8, MCART_1:def_9; A6: ( s = y9 `3_4 & t = y9 `4_4 ) by MCART_1:def_10, MCART_1:def_11; hence y in X by A1, A5; ::_thesis: S2[y,x] thus S2[y,x] by A5, A6; ::_thesis: verum end; hence x in Y by A3; ::_thesis: verum end; 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 proof defpred S1[ set ] means \$1 is strict Subgraph of G; let X1, X2 be set ; ::_thesis: ( ( for x being set holds ( x in X1 iff x is strict Subgraph of G ) ) & ( for x being set holds ( x in X2 iff x is strict Subgraph of G ) ) implies X1 = X2 ) assume that A7: for x being set holds ( x in X1 iff S1[x] ) and A8: for x being set holds ( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2 thus X1 = X2 from XBOOLE_0:sch_2(A7, A8); ::_thesis: verum end; 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] ) ) proof consider X being set such that A1: for x being set holds ( x in X iff ( x in bool F1() & P1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ( x is strict Subgraph of F1() & P1[x] ) ) let x be set ; ::_thesis: ( x in X iff ( x is strict Subgraph of F1() & P1[x] ) ) thus ( x in X implies ( x is strict Subgraph of F1() & P1[x] ) ) ::_thesis: ( x is strict Subgraph of F1() & P1[x] implies x in X ) proof assume A2: x in X ; ::_thesis: ( x is strict Subgraph of F1() & P1[x] ) then x in bool F1() by A1; hence x is strict Subgraph of F1() by Def25; ::_thesis: P1[x] thus P1[x] by A1, A2; ::_thesis: verum end; assume that A3: x is strict Subgraph of F1() and A4: P1[x] ; ::_thesis: x in X x in bool F1() by A3, Def25; hence x in X by A1, A4; ::_thesis: verum end; 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; 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; 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 ) proof let G1, G be Graph; ::_thesis: ( G1 c= G implies ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G ) ) assume G1 c= G ; ::_thesis: ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G ) then A1: G1 is Subgraph of G by Def24; for v being set st v in the Source of G1 holds v in the Source of G proof let v be set ; ::_thesis: ( v in the Source of G1 implies v in the Source of G ) assume A2: v in the Source of G1 ; ::_thesis: v in the Source of G then consider x, y being set such that A3: [x,y] = v by RELAT_1:def_1; A4: x in dom the Source of G1 by A2, A3, FUNCT_1:1; A5: y = the Source of G1 . x by A2, A3, FUNCT_1:1; A6: x in the carrier' of G1 by A4; the carrier' of G1 c= the carrier' of G by A1, Def18; then x in the carrier' of G by A6; then A7: x in dom the Source of G by FUNCT_2:def_1; y = the Source of G . x by A1, A4, A5, Def18; hence v in the Source of G by A3, A7, FUNCT_1:def_2; ::_thesis: verum end; hence the Source of G1 c= the Source of G by TARSKI:def_3; ::_thesis: the Target of G1 c= the Target of G for v being set st v in the Target of G1 holds v in the Target of G proof let v be set ; ::_thesis: ( v in the Target of G1 implies v in the Target of G ) assume A8: v in the Target of G1 ; ::_thesis: v in the Target of G then consider x, y being set such that A9: [x,y] = v by RELAT_1:def_1; A10: x in dom the Target of G1 by A8, A9, FUNCT_1:1; A11: y = the Target of G1 . x by A8, A9, FUNCT_1:1; A12: x in the carrier' of G1 by A10; the carrier' of G1 c= the carrier' of G by A1, Def18; then x in the carrier' of G by A12; then A13: x in dom the Target of G by FUNCT_2:def_1; y = the Target of G . x by A1, A10, A11, Def18; hence v in the Target of G by A9, A13, FUNCT_1:def_2; ::_thesis: verum end; hence the Target of G1 c= the Target of G by TARSKI:def_3; ::_thesis: verum end; 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 ) proof let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( 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 ) ) assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( 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 ) set S12 = the Source of (G1 \/ G2); set S1 = the Source of G1; set S2 = the Source of G2; set T12 = the Target of (G1 \/ G2); set T1 = the Target of G1; set T2 = the Target of G2; for v being set holds ( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 ) proof let v be set ; ::_thesis: ( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 ) thus ( v in the Source of (G1 \/ G2) implies v in the Source of G1 \/ the Source of G2 ) ::_thesis: ( v in the Source of G1 \/ the Source of G2 implies v in the Source of (G1 \/ G2) ) proof assume A2: v in the Source of (G1 \/ G2) ; ::_thesis: v in the Source of G1 \/ the Source of G2 then consider x, y being set such that A3: [x,y] = v by RELAT_1:def_1; x in dom the Source of (G1 \/ G2) by A2, A3, FUNCT_1:1; then x in the carrier' of (G1 \/ G2) ; then A4: x in the carrier' of G1 \/ the carrier' of G2 by A1, Def5; A5: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_[x,y]_in_the_Source_of_G1_\/_the_Source_of_G2_) assume A6: x in the carrier' of G1 ; ::_thesis: [x,y] in the Source of G1 \/ the Source of G2 then A7: x in dom the Source of G1 by FUNCT_2:def_1; the Source of G1 . x = the Source of (G1 \/ G2) . x by A1, A6, Def5 .= y by A2, A3, FUNCT_1:1 ; then ( [x,y] in the Source of G1 or [x,y] in the Source of G2 ) by A7, FUNCT_1:def_2; hence [x,y] in the Source of G1 \/ the Source of G2 by XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_[x,y]_in_the_Source_of_G1_\/_the_Source_of_G2_) assume A8: x in the carrier' of G2 ; ::_thesis: [x,y] in the Source of G1 \/ the Source of G2 then A9: x in dom the Source of G2 by FUNCT_2:def_1; the Source of G2 . x = the Source of (G1 \/ G2) . x by A1, A8, Def5 .= y by A2, A3, FUNCT_1:1 ; then ( [x,y] in the Source of G1 or [x,y] in the Source of G2 ) by A9, FUNCT_1:def_2; hence [x,y] in the Source of G1 \/ the Source of G2 by XBOOLE_0:def_3; ::_thesis: verum end; hence v in the Source of G1 \/ the Source of G2 by A3, A4, A5, XBOOLE_0:def_3; ::_thesis: verum end; assume A10: v in the Source of G1 \/ the Source of G2 ; ::_thesis: v in the Source of (G1 \/ G2) A11: now__::_thesis:_(_v_in_the_Source_of_G1_implies_v_in_the_Source_of_(G1_\/_G2)_) assume A12: v in the Source of G1 ; ::_thesis: v in the Source of (G1 \/ G2) then consider x, y being set such that A13: [x,y] = v by RELAT_1:def_1; A14: x in dom the Source of G1 by A12, A13, FUNCT_1:1; A15: y = the Source of G1 . x by A12, A13, FUNCT_1:1; x in the carrier' of G1 \/ the carrier' of G2 by A14, XBOOLE_0:def_3; then x in the carrier' of (G1 \/ G2) by A1, Def5; then A16: x in dom the Source of (G1 \/ G2) by FUNCT_2:def_1; the Source of (G1 \/ G2) . x = y by A1, A14, A15, Def5; hence v in the Source of (G1 \/ G2) by A13, A16, FUNCT_1:def_2; ::_thesis: verum end; now__::_thesis:_(_v_in_the_Source_of_G2_implies_v_in_the_Source_of_(G1_\/_G2)_) assume A17: v in the Source of G2 ; ::_thesis: v in the Source of (G1 \/ G2) then consider x, y being set such that A18: [x,y] = v by RELAT_1:def_1; A19: x in dom the Source of G2 by A17, A18, FUNCT_1:1; A20: y = the Source of G2 . x by A17, A18, FUNCT_1:1; x in the carrier' of G1 \/ the carrier' of G2 by A19, XBOOLE_0:def_3; then x in the carrier' of (G1 \/ G2) by A1, Def5; then A21: x in dom the Source of (G1 \/ G2) by FUNCT_2:def_1; the Source of (G1 \/ G2) . x = y by A1, A19, A20, Def5; hence v in the Source of (G1 \/ G2) by A18, A21, FUNCT_1:def_2; ::_thesis: verum end; hence v in the Source of (G1 \/ G2) by A10, A11, XBOOLE_0:def_3; ::_thesis: verum end; hence the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 by TARSKI:1; ::_thesis: the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 for v being set holds ( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 ) proof let v be set ; ::_thesis: ( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 ) thus ( v in the Target of (G1 \/ G2) implies v in the Target of G1 \/ the Target of G2 ) ::_thesis: ( v in the Target of G1 \/ the Target of G2 implies v in the Target of (G1 \/ G2) ) proof assume A22: v in the Target of (G1 \/ G2) ; ::_thesis: v in the Target of G1 \/ the Target of G2 then consider x, y being set such that A23: [x,y] = v by RELAT_1:def_1; x in dom the Target of (G1 \/ G2) by A22, A23, FUNCT_1:1; then x in the carrier' of (G1 \/ G2) ; then A24: x in the carrier' of G1 \/ the carrier' of G2 by A1, Def5; A25: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_[x,y]_in_the_Target_of_G1_\/_the_Target_of_G2_) assume A26: x in the carrier' of G1 ; ::_thesis: [x,y] in the Target of G1 \/ the Target of G2 then A27: x in dom the Target of G1 by FUNCT_2:def_1; the Target of G1 . x = the Target of (G1 \/ G2) . x by A1, A26, Def5 .= y by A22, A23, FUNCT_1:1 ; then ( [x,y] in the Target of G1 or [x,y] in the Target of G2 ) by A27, FUNCT_1:def_2; hence [x,y] in the Target of G1 \/ the Target of G2 by XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_[x,y]_in_the_Target_of_G1_\/_the_Target_of_G2_) assume A28: x in the carrier' of G2 ; ::_thesis: [x,y] in the Target of G1 \/ the Target of G2 then A29: x in dom the Target of G2 by FUNCT_2:def_1; the Target of G2 . x = the Target of (G1 \/ G2) . x by A1, A28, Def5 .= y by A22, A23, FUNCT_1:1 ; then ( [x,y] in the Target of G1 or [x,y] in the Target of G2 ) by A29, FUNCT_1:def_2; hence [x,y] in the Target of G1 \/ the Target of G2 by XBOOLE_0:def_3; ::_thesis: verum end; hence v in the Target of G1 \/ the Target of G2 by A23, A24, A25, XBOOLE_0:def_3; ::_thesis: verum end; assume A30: v in the Target of G1 \/ the Target of G2 ; ::_thesis: v in the Target of (G1 \/ G2) A31: now__::_thesis:_(_v_in_the_Target_of_G1_implies_v_in_the_Target_of_(G1_\/_G2)_) assume A32: v in the Target of G1 ; ::_thesis: v in the Target of (G1 \/ G2) then consider x, y being set such that A33: [x,y] = v by RELAT_1:def_1; A34: x in dom the Target of G1 by A32, A33, FUNCT_1:1; A35: y = the Target of G1 . x by A32, A33, FUNCT_1:1; x in the carrier' of G1 \/ the carrier' of G2 by A34, XBOOLE_0:def_3; then x in the carrier' of (G1 \/ G2) by A1, Def5; then A36: x in dom the Target of (G1 \/ G2) by FUNCT_2:def_1; the Target of (G1 \/ G2) . x = y by A1, A34, A35, Def5; hence v in the Target of (G1 \/ G2) by A33, A36, FUNCT_1:def_2; ::_thesis: verum end; now__::_thesis:_(_v_in_the_Target_of_G2_implies_v_in_the_Target_of_(G1_\/_G2)_) assume A37: v in the Target of G2 ; ::_thesis: v in the Target of (G1 \/ G2) then consider x, y being set such that A38: [x,y] = v by RELAT_1:def_1; A39: x in dom the Target of G2 by A37, A38, FUNCT_1:1; A40: y = the Target of G2 . x by A37, A38, FUNCT_1:1; x in the carrier' of G1 \/ the carrier' of G2 by A39, XBOOLE_0:def_3; then x in the carrier' of (G1 \/ G2) by A1, Def5; then A41: x in dom the Target of (G1 \/ G2) by FUNCT_2:def_1; the Target of (G1 \/ G2) . x = y by A1, A39, A40, Def5; hence v in the Target of (G1 \/ G2) by A38, A41, FUNCT_1:def_2; ::_thesis: verum end; hence v in the Target of (G1 \/ G2) by A30, A31, XBOOLE_0:def_3; ::_thesis: verum end; hence the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 by TARSKI:1; ::_thesis: verum end; theorem Th7: :: GRAPH_1:7 for G being strict Graph holds G = G \/ G proof let G be strict Graph; ::_thesis: G = G \/ G A1: the carrier of (G \/ G) = the carrier of G \/ the carrier of G by Def5 .= the carrier of G ; A2: the carrier' of (G \/ G) = the carrier' of G \/ the carrier' of G by Def5 .= the carrier' of G ; then A3: dom the Source of G = the carrier' of (G \/ G) by FUNCT_2:def_1 .= dom the Source of (G \/ G) by FUNCT_2:def_1 ; for v being set st v in dom the Source of G holds the Source of G . v = the Source of (G \/ G) . v by Def5; then A4: the Source of G = the Source of (G \/ G) by A3, FUNCT_1:2; A5: dom the Target of G = the carrier' of (G \/ G) by A2, FUNCT_2:def_1 .= dom the Target of (G \/ G) by FUNCT_2:def_1 ; for v being set st v in dom the Target of G holds the Target of G . v = the Target of (G \/ G) . v by Def5; hence G = G \/ G by A1, A2, A4, A5, FUNCT_1:2; ::_thesis: verum end; 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 proof let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies G1 \/ G2 = G2 \/ G1 ) assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: G1 \/ G2 = G2 \/ G1 then A2: the carrier of (G1 \/ G2) = the carrier of G2 \/ the carrier of G1 by Def5 .= the carrier of (G2 \/ G1) by A1, Def5 ; A3: the carrier' of (G1 \/ G2) = the carrier' of G2 \/ the carrier' of G1 by A1, Def5 .= the carrier' of (G2 \/ G1) by A1, Def5 ; then A4: dom the Source of (G1 \/ G2) = the carrier' of (G2 \/ G1) by FUNCT_2:def_1 .= dom the Source of (G2 \/ G1) by FUNCT_2:def_1 ; for v being set st v in dom the Source of (G1 \/ G2) holds the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v proof let v be set ; ::_thesis: ( v in dom the Source of (G1 \/ G2) implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v ) assume v in dom the Source of (G1 \/ G2) ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v then v in the carrier' of (G1 \/ G2) ; then A5: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5; A6: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_(G2_\/_G1)_._v_) assume A7: v in the carrier' of G1 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v hence the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, Def5 .= the Source of (G2 \/ G1) . v by A1, A7, Def5 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_(G2_\/_G1)_._v_) assume A8: v in the carrier' of G2 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v hence the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, Def5 .= the Source of (G2 \/ G1) . v by A1, A8, Def5 ; ::_thesis: verum end; hence the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v by A5, A6, XBOOLE_0:def_3; ::_thesis: verum end; then A9: the Source of (G1 \/ G2) = the Source of (G2 \/ G1) by A4, FUNCT_1:2; A10: dom the Target of (G1 \/ G2) = the carrier' of (G2 \/ G1) by A3, FUNCT_2:def_1 .= dom the Target of (G2 \/ G1) by FUNCT_2:def_1 ; for v being set st v in dom the Target of (G1 \/ G2) holds the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v proof let v be set ; ::_thesis: ( v in dom the Target of (G1 \/ G2) implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v ) assume v in dom the Target of (G1 \/ G2) ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v then v in the carrier' of (G1 \/ G2) ; then A11: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5; A12: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_(G2_\/_G1)_._v_) assume A13: v in the carrier' of G1 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v hence the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, Def5 .= the Target of (G2 \/ G1) . v by A1, A13, Def5 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_(G2_\/_G1)_._v_) assume A14: v in the carrier' of G2 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v hence the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, Def5 .= the Target of (G2 \/ G1) . v by A1, A14, Def5 ; ::_thesis: verum end; hence the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v by A11, A12, XBOOLE_0:def_3; ::_thesis: verum end; hence G1 \/ G2 = G2 \/ G1 by A2, A3, A9, A10, FUNCT_1:2; ::_thesis: verum end; 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) proof let G1, G2, G3 be Graph; ::_thesis: ( 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 implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) ) assume that A1: the Source of G1 tolerates the Source of G2 and A2: the Target of G1 tolerates the Target of G2 and A3: the Source of G1 tolerates the Source of G3 and A4: the Target of G1 tolerates the Target of G3 and A5: the Source of G2 tolerates the Source of G3 and A6: the Target of G2 tolerates the Target of G3 ; ::_thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) A7: for v being set st v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) holds the Source of (G1 \/ G2) . v = the Source of G3 . v proof let v be set ; ::_thesis: ( v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) implies the Source of (G1 \/ G2) . v = the Source of G3 . v ) assume A8: v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v then A9: v in dom the Source of G3 by XBOOLE_0:def_4; v in dom the Source of (G1 \/ G2) by A8, XBOOLE_0:def_4; then v in the carrier' of (G1 \/ G2) ; then A10: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5; A11: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_) assume A12: v in the carrier' of G1 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v then v in dom the Source of G1 by FUNCT_2:def_1; then A13: v in (dom the Source of G1) /\ (dom the Source of G3) by A9, XBOOLE_0:def_4; thus the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, A2, A12, Def5 .= the Source of G3 . v by A3, A13, PARTFUN1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_) assume A14: v in the carrier' of G2 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v then v in dom the Source of G2 by FUNCT_2:def_1; then A15: v in (dom the Source of G2) /\ (dom the Source of G3) by A9, XBOOLE_0:def_4; thus the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, A2, A14, Def5 .= the Source of G3 . v by A5, A15, PARTFUN1:def_4 ; ::_thesis: verum end; hence the Source of (G1 \/ G2) . v = the Source of G3 . v by A10, A11, XBOOLE_0:def_3; ::_thesis: verum end; A16: for v being set st v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) holds the Target of (G1 \/ G2) . v = the Target of G3 . v proof let v be set ; ::_thesis: ( v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) implies the Target of (G1 \/ G2) . v = the Target of G3 . v ) assume A17: v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v then A18: v in dom the Target of G3 by XBOOLE_0:def_4; v in dom the Target of (G1 \/ G2) by A17, XBOOLE_0:def_4; then v in the carrier' of (G1 \/ G2) ; then A19: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5; A20: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_) assume A21: v in the carrier' of G1 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v then v in dom the Target of G1 by FUNCT_2:def_1; then A22: v in (dom the Target of G1) /\ (dom the Target of G3) by A18, XBOOLE_0:def_4; thus the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, A2, A21, Def5 .= the Target of G3 . v by A4, A22, PARTFUN1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_) assume A23: v in the carrier' of G2 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v then v in dom the Target of G2 by FUNCT_2:def_1; then A24: v in (dom the Target of G2) /\ (dom the Target of G3) by A18, XBOOLE_0:def_4; thus the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, A2, A23, Def5 .= the Target of G3 . v by A6, A24, PARTFUN1:def_4 ; ::_thesis: verum end; hence the Target of (G1 \/ G2) . v = the Target of G3 . v by A19, A20, XBOOLE_0:def_3; ::_thesis: verum end; A25: the Source of (G1 \/ G2) tolerates the Source of G3 by A7, PARTFUN1:def_4; A26: the Target of (G1 \/ G2) tolerates the Target of G3 by A16, PARTFUN1:def_4; A27: for v being set st v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) holds the Source of G1 . v = the Source of (G2 \/ G3) . v proof let v be set ; ::_thesis: ( v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) implies the Source of G1 . v = the Source of (G2 \/ G3) . v ) assume A28: v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) ; ::_thesis: the Source of G1 . v = the Source of (G2 \/ G3) . v then A29: v in dom the Source of G1 by XBOOLE_0:def_4; v in the carrier' of (G2 \/ G3) by A28; then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5; then v in the carrier' of G2 \/ (dom the Source of G3) by FUNCT_2:def_1; then A30: v in (dom the Source of G2) \/ (dom the Source of G3) by FUNCT_2:def_1; A31: now__::_thesis:_(_v_in_dom_the_Source_of_G2_implies_the_Source_of_(G2_\/_G3)_._v_=_the_Source_of_G1_._v_) assume A32: v in dom the Source of G2 ; ::_thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v then A33: v in (dom the Source of G1) /\ (dom the Source of G2) by A29, XBOOLE_0:def_4; thus the Source of (G2 \/ G3) . v = the Source of G2 . v by A5, A6, A32, Def5 .= the Source of G1 . v by A1, A33, PARTFUN1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_v_in_dom_the_Source_of_G3_implies_the_Source_of_(G2_\/_G3)_._v_=_the_Source_of_G1_._v_) assume A34: v in dom the Source of G3 ; ::_thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v then A35: v in (dom the Source of G1) /\ (dom the Source of G3) by A29, XBOOLE_0:def_4; thus the Source of (G2 \/ G3) . v = the Source of G3 . v by A5, A6, A34, Def5 .= the Source of G1 . v by A3, A35, PARTFUN1:def_4 ; ::_thesis: verum end; hence the Source of G1 . v = the Source of (G2 \/ G3) . v by A30, A31, XBOOLE_0:def_3; ::_thesis: verum end; A36: for v being set st v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) holds the Target of G1 . v = the Target of (G2 \/ G3) . v proof let v be set ; ::_thesis: ( v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) implies the Target of G1 . v = the Target of (G2 \/ G3) . v ) assume A37: v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) ; ::_thesis: the Target of G1 . v = the Target of (G2 \/ G3) . v then A38: v in dom the Target of G1 by XBOOLE_0:def_4; v in the carrier' of (G2 \/ G3) by A37; then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5; then v in the carrier' of G2 \/ (dom the Target of G3) by FUNCT_2:def_1; then A39: v in (dom the Target of G2) \/ (dom the Target of G3) by FUNCT_2:def_1; A40: now__::_thesis:_(_v_in_dom_the_Target_of_G2_implies_the_Target_of_(G2_\/_G3)_._v_=_the_Target_of_G1_._v_) assume A41: v in dom the Target of G2 ; ::_thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v then A42: v in (dom the Target of G1) /\ (dom the Target of G2) by A38, XBOOLE_0:def_4; thus the Target of (G2 \/ G3) . v = the Target of G2 . v by A5, A6, A41, Def5 .= the Target of G1 . v by A2, A42, PARTFUN1:def_4 ; ::_thesis: verum end; now__::_thesis:_(_v_in_dom_the_Target_of_G3_implies_the_Target_of_(G2_\/_G3)_._v_=_the_Target_of_G1_._v_) assume A43: v in dom the Target of G3 ; ::_thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v then A44: v in (dom the Target of G1) /\ (dom the Target of G3) by A38, XBOOLE_0:def_4; thus the Target of (G2 \/ G3) . v = the Target of G3 . v by A5, A6, A43, Def5 .= the Target of G1 . v by A4, A44, PARTFUN1:def_4 ; ::_thesis: verum end; hence the Target of G1 . v = the Target of (G2 \/ G3) . v by A39, A40, XBOOLE_0:def_3; ::_thesis: verum end; A45: the Source of G1 tolerates the Source of (G2 \/ G3) by A27, PARTFUN1:def_4; A46: the Target of G1 tolerates the Target of (G2 \/ G3) by A36, PARTFUN1:def_4; A47: the carrier' of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5 .= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5 .= the carrier' of G1 \/ ( the carrier' of G2 \/ the carrier' of G3) by XBOOLE_1:4 .= the carrier' of G1 \/ the carrier' of (G2 \/ G3) by A5, A6, Def5 .= the carrier' of (G1 \/ (G2 \/ G3)) by A45, A46, Def5 ; A48: the carrier of ((G1 \/ G2) \/ G3) = the carrier of (G1 \/ G2) \/ the carrier of G3 by A25, A26, Def5 .= ( the carrier of G1 \/ the carrier of G2) \/ the carrier of G3 by A1, A2, Def5 .= the carrier of G1 \/ ( the carrier of G2 \/ the carrier of G3) by XBOOLE_1:4 .= the carrier of G1 \/ the carrier of (G2 \/ G3) by A5, A6, Def5 .= the carrier of (G1 \/ (G2 \/ G3)) by A45, A46, Def5 ; A49: dom the Source of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A47, FUNCT_2:def_1 .= dom the Source of (G1 \/ (G2 \/ G3)) by FUNCT_2:def_1 ; for v being set st v in dom the Source of ((G1 \/ G2) \/ G3) holds the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v proof let v be set ; ::_thesis: ( v in dom the Source of ((G1 \/ G2) \/ G3) implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v ) assume A50: v in dom the Source of ((G1 \/ G2) \/ G3) ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v dom the Source of ((G1 \/ G2) \/ G3) = the carrier' of ((G1 \/ G2) \/ G3) by FUNCT_2:def_1 .= the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5 .= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5 ; then A51: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A50, XBOOLE_0:def_3; A52: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_) assume A53: v in the carrier' of G1 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v the carrier' of G1 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7; then the carrier' of G1 c= the carrier' of (G1 \/ G2) by A1, A2, Def5; hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A25, A26, A53, Def5 .= the Source of G1 . v by A1, A2, A53, Def5 .= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A53, Def5 ; ::_thesis: verum end; A54: now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_) assume A55: v in the carrier' of G2 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v the carrier' of G2 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7; then A56: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, A2, Def5; the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7; then A57: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A5, A6, Def5; thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A25, A26, A55, A56, Def5 .= the Source of G2 . v by A1, A2, A55, Def5 .= the Source of (G2 \/ G3) . v by A5, A6, A55, Def5 .= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A55, A57, Def5 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G3_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_) assume A58: v in the carrier' of G3 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v the carrier' of G3 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7; then A59: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A5, A6, Def5; thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of G3 . v by A25, A26, A58, Def5 .= the Source of (G2 \/ G3) . v by A5, A6, A58, Def5 .= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A58, A59, Def5 ; ::_thesis: verum end; hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v by A51, A52, A54, XBOOLE_0:def_3; ::_thesis: verum end; then A60: the Source of ((G1 \/ G2) \/ G3) = the Source of (G1 \/ (G2 \/ G3)) by A49, FUNCT_1:2; A61: dom the Target of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A47, FUNCT_2:def_1 .= dom the Target of (G1 \/ (G2 \/ G3)) by FUNCT_2:def_1 ; for v being set st v in dom the Target of ((G1 \/ G2) \/ G3) holds the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v proof let v be set ; ::_thesis: ( v in dom the Target of ((G1 \/ G2) \/ G3) implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v ) assume A62: v in dom the Target of ((G1 \/ G2) \/ G3) ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v dom the Target of ((G1 \/ G2) \/ G3) = the carrier' of ((G1 \/ G2) \/ G3) by FUNCT_2:def_1 .= the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5 .= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5 ; then A63: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A62, XBOOLE_0:def_3; A64: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_) assume A65: v in the carrier' of G1 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v the carrier' of G1 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7; then the carrier' of G1 c= the carrier' of (G1 \/ G2) by A1, A2, Def5; hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A25, A26, A65, Def5 .= the Target of G1 . v by A1, A2, A65, Def5 .= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A65, Def5 ; ::_thesis: verum end; A66: now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_) assume A67: v in the carrier' of G2 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v the carrier' of G2 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7; then A68: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, A2, Def5; the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7; then A69: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A5, A6, Def5; thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A25, A26, A67, A68, Def5 .= the Target of G2 . v by A1, A2, A67, Def5 .= the Target of (G2 \/ G3) . v by A5, A6, A67, Def5 .= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A67, A69, Def5 ; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G3_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_) assume A70: v in the carrier' of G3 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v the carrier' of G3 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7; then A71: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A5, A6, Def5; thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of G3 . v by A25, A26, A70, Def5 .= the Target of (G2 \/ G3) . v by A5, A6, A70, Def5 .= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A70, A71, Def5 ; ::_thesis: verum end; hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v by A63, A64, A66, XBOOLE_0:def_3; ::_thesis: verum end; hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A47, A48, A60, A61, FUNCT_1:2; ::_thesis: verum end; 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 proof let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies G is_sum_of G2,G1 ) assume A1: G is_sum_of G1,G2 ; ::_thesis: G is_sum_of G2,G1 then A2: the Target of G1 tolerates the Target of G2 by Def6; A3: ( 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 ) by A1, Def6; A4: the Source of G2 tolerates the Source of G1 by A1, Def6; MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G2 \/ G1 by A2, A3, Th8; hence G is_sum_of G2,G1 by A2, A4, Def6; ::_thesis: verum end; theorem :: GRAPH_1:11 for G being strict Graph holds G is_sum_of G,G proof let G be strict Graph; ::_thesis: G is_sum_of G,G G = G \/ G by Th7; hence G is_sum_of G,G by Def6; ::_thesis: verum end; 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 proof let G1, G2 be Graph; ::_thesis: ( ex G being Graph st ( G1 c= G & G2 c= G ) implies G1 \/ G2 = G2 \/ G1 ) given G being Graph such that A1: ( G1 c= G & G2 c= G ) ; ::_thesis: G1 \/ G2 = G2 \/ G1 A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by A1, Th5; A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5; A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:52; the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:52; hence G1 \/ G2 = G2 \/ G1 by A4, Th8; ::_thesis: verum end; 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) proof let G1, G2, G3 be Graph; ::_thesis: ( ex G being Graph st ( G1 c= G & G2 c= G & G3 c= G ) implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) ) given G being Graph such that A1: G1 c= G and A2: G2 c= G and A3: G3 c= G ; ::_thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) A4: the Source of G1 c= the Source of G by A1, Th5; A5: the Source of G2 c= the Source of G by A2, Th5; A6: the Source of G3 c= the Source of G by A3, Th5; A7: the Target of G1 c= the Target of G by A1, Th5; A8: the Target of G2 c= the Target of G by A2, Th5; A9: the Target of G3 c= the Target of G by A3, Th5; A10: the Source of G1 tolerates the Source of G2 by A4, A5, PARTFUN1:57; A11: the Source of G1 tolerates the Source of G3 by A4, A6, PARTFUN1:57; A12: the Source of G2 tolerates the Source of G3 by A5, A6, PARTFUN1:57; A13: the Target of G1 tolerates the Target of G2 by A7, A8, PARTFUN1:57; A14: the Target of G1 tolerates the Target of G3 by A7, A9, PARTFUN1:57; the Target of G2 tolerates the Target of G3 by A8, A9, PARTFUN1:57; hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A10, A11, A12, A13, A14, Th9; ::_thesis: verum end; 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 proof let G1, G2 be strict Graph; ::_thesis: ( G1 c= G2 & G2 c= G1 implies G1 = G2 ) assume that A1: G1 c= G2 and A2: G2 c= G1 ; ::_thesis: G1 = G2 A3: G1 is Subgraph of G2 by A1, Def24; A4: G2 is Subgraph of G1 by A2, Def24; A5: the carrier of G1 c= the carrier of G2 by A3, Def18; the carrier of G2 c= the carrier of G1 by A4, Def18; then A6: the carrier of G1 = the carrier of G2 by A5, XBOOLE_0:def_10; A7: the carrier' of G1 c= the carrier' of G2 by A3, Def18; the carrier' of G2 c= the carrier' of G1 by A4, Def18; then A8: the carrier' of G1 = the carrier' of G2 by A7, XBOOLE_0:def_10; then A9: dom the Source of G1 = the carrier' of G2 by FUNCT_2:def_1 .= dom the Source of G2 by FUNCT_2:def_1 ; for v being set st v in dom the Source of G1 holds the Source of G1 . v = the Source of G2 . v by A3, Def18; then A10: the Source of G1 = the Source of G2 by A9, FUNCT_1:2; A11: dom the Target of G1 = the carrier' of G2 by A8, FUNCT_2:def_1 .= dom the Target of G2 by FUNCT_2:def_1 ; for v being set st v in dom the Target of G1 holds the Target of G1 . v = the Target of G2 . v by A3, Def18; hence G1 = G2 by A6, A8, A10, A11, FUNCT_1:2; ::_thesis: verum end; theorem Th17: :: GRAPH_1:17 for G1, G2, G3 being Graph st G1 c= G2 & G2 c= G3 holds G1 c= G3 proof let G1, G2, G3 be Graph; ::_thesis: ( G1 c= G2 & G2 c= G3 implies G1 c= G3 ) assume that A1: G1 c= G2 and A2: G2 c= G3 ; ::_thesis: G1 c= G3 A3: G1 is Subgraph of G2 by A1, Def24; A4: G2 is Subgraph of G3 by A2, Def24; A5: the carrier of G1 c= the carrier of G2 by A3, Def18; the carrier of G2 c= the carrier of G3 by A4, Def18; then A6: the carrier of G1 c= the carrier of G3 by A5, XBOOLE_1:1; A7: the carrier' of G1 c= the carrier' of G2 by A3, Def18; the carrier' of G2 c= the carrier' of G3 by A4, Def18; then A8: the carrier' of G1 c= the carrier' of G3 by A7, XBOOLE_1:1; for v being set st v in the carrier' of G1 holds ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) proof let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) ) assume A9: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) hence A10: the Source of G1 . v = the Source of G2 . v by A3, Def18 .= the Source of G3 . v by A4, A7, A9, Def18 ; ::_thesis: ( the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) thus A11: the Target of G1 . v = the Target of G2 . v by A3, A9, Def18 .= the Target of G3 . v by A4, A7, A9, Def18 ; ::_thesis: ( the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) v in dom the Source of G1 by A9, FUNCT_2:def_1; then the Source of G1 . v in rng the Source of G1 by FUNCT_1:def_3; hence the Source of G3 . v in the carrier of G1 by A10; ::_thesis: the Target of G3 . v in the carrier of G1 v in dom the Target of G1 by A9, FUNCT_2:def_1; then the Target of G1 . v in rng the Target of G1 by FUNCT_1:def_3; hence the Target of G3 . v in the carrier of G1 by A11; ::_thesis: verum end; then G1 is Subgraph of G3 by A6, A8, Def18; hence G1 c= G3 by Def24; ::_thesis: verum end; 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 ) proof let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies ( G1 c= G & G2 c= G ) ) assume A1: G is_sum_of G1,G2 ; ::_thesis: ( G1 c= G & G2 c= G ) A2: for G, G1, G2 being Graph st G is_sum_of G1,G2 holds G1 c= G proof let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies G1 c= G ) assume A3: G is_sum_of G1,G2 ; ::_thesis: G1 c= G then A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by Def6; A5: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A3, Def6; then the carrier of G = the carrier of G1 \/ the carrier of G2 by A4, Def5; then A6: the carrier of G1 c= the carrier of G by XBOOLE_1:7; the carrier' of G = the carrier' of G1 \/ the carrier' of G2 by A4, A5, Def5; then A7: the carrier' of G1 c= the carrier' of G by XBOOLE_1:7; for v being set st v in the carrier' of G1 holds ( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) proof let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) ) assume A8: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) hence A9: the Source of G1 . v = the Source of G . v by A4, A5, Def5; ::_thesis: ( the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) thus A10: the Target of G1 . v = the Target of G . v by A4, A5, A8, Def5; ::_thesis: ( the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) thus the Source of G . v in the carrier of G1 by A8, A9, FUNCT_2:5; ::_thesis: the Target of G . v in the carrier of G1 thus the Target of G . v in the carrier of G1 by A8, A10, FUNCT_2:5; ::_thesis: verum end; then G1 is Subgraph of G by A6, A7, Def18; hence G1 c= G by Def24; ::_thesis: verum end; hence G1 c= G by A1; ::_thesis: G2 c= G thus G2 c= G by A1, A2, Th10; ::_thesis: verum end; 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 ) proof let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) ) assume ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) then G1 \/ G2 is_sum_of G1,G2 by Def6; hence ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) by Th18; ::_thesis: verum end; 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 ) proof let G1, G2 be Graph; ::_thesis: ( ex G being Graph st ( G1 c= G & G2 c= G ) implies ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) ) given G being Graph such that A1: ( G1 c= G & G2 c= G ) ; ::_thesis: ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by A1, Th5; A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5; A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:57; the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:57; hence ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) by A4, Th19; ::_thesis: verum end; 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 proof let G1, G3, G2, G be Graph; ::_thesis: ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 implies G c= G3 ) assume that A1: G1 c= G3 and A2: G2 c= G3 and A3: G is_sum_of G1,G2 ; ::_thesis: G c= G3 A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A3, Def6; A5: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A3, Def6; A6: G1 is Subgraph of G3 by A1, Def24; A7: G2 is Subgraph of G3 by A2, Def24; A8: the carrier of G1 c= the carrier of G3 by A6, Def18; the carrier of G2 c= the carrier of G3 by A7, Def18; then A9: the carrier of G1 \/ the carrier of G2 c= the carrier of G3 by A8, XBOOLE_1:8; A10: the carrier' of G1 c= the carrier' of G3 by A6, Def18; the carrier' of G2 c= the carrier' of G3 by A7, Def18; then A11: the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3 by A10, XBOOLE_1:8; for v being set st v in the carrier' of (G1 \/ G2) holds ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) proof let v be set ; ::_thesis: ( v in the carrier' of (G1 \/ G2) implies ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) ) assume A12: v in the carrier' of (G1 \/ G2) ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) thus A13: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) ::_thesis: ( the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) proof A14: v in the carrier' of G1 \/ the carrier' of G2 by A4, A12, Def5; A15: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_(_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_&_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)_) assume A16: v in the carrier' of G1 ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) then A17: the Source of G3 . v = the Source of G1 . v by A6, Def18 .= the Source of (G1 \/ G2) . v by A4, A16, Def5 ; the Target of G3 . v = the Target of G1 . v by A6, A16, Def18 .= the Target of (G1 \/ G2) . v by A4, A16, Def5 ; hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A17; ::_thesis: verum end; now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_(_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_&_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)_) assume A18: v in the carrier' of G2 ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) then A19: the Source of G3 . v = the Source of G2 . v by A7, Def18 .= the Source of (G1 \/ G2) . v by A4, A18, Def5 ; the Target of G3 . v = the Target of G2 . v by A7, A18, Def18 .= the Target of (G1 \/ G2) . v by A4, A18, Def5 ; hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A19; ::_thesis: verum end; hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A14, A15, XBOOLE_0:def_3; ::_thesis: verum end; hence the Source of G3 . v in the carrier of (G1 \/ G2) by A12, FUNCT_2:5; ::_thesis: the Target of G3 . v in the carrier of (G1 \/ G2) thus the Target of G3 . v in the carrier of (G1 \/ G2) by A12, A13, FUNCT_2:5; ::_thesis: verum end; hence ( the carrier of G c= the carrier of G3 & the carrier' of G c= the carrier' of G3 & ( for v being set st v in the carrier' of G holds ( the Source of G . v = the Source of G3 . v & the Target of G . v = the Target of G3 . v & the Source of G3 . v in the carrier of G & the Target of G3 . v in the carrier of G ) ) ) by A4, A5, A9, A11, Def5; :: according to GRAPH_1:def_18,GRAPH_1:def_24 ::_thesis: verum end; theorem Th22: :: GRAPH_1:22 for G1, G, G2 being Graph st G1 c= G & G2 c= G holds G1 \/ G2 c= G proof let G1, G, G2 be Graph; ::_thesis: ( G1 c= G & G2 c= G implies G1 \/ G2 c= G ) assume A1: ( G1 c= G & G2 c= G ) ; ::_thesis: G1 \/ G2 c= G then A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by Th5; A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5; A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:57; the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:57; then G1 \/ G2 is_sum_of G1,G2 by A4, Def6; hence G1 \/ G2 c= G by A1, Th21; ::_thesis: verum end; theorem :: GRAPH_1:23 for G1, G2 being strict Graph st G1 c= G2 holds ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) proof let G1, G2 be strict Graph; ::_thesis: ( G1 c= G2 implies ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) ) assume A1: G1 c= G2 ; ::_thesis: ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) then ( G1 \/ G2 c= G2 & G2 c= G1 \/ G2 ) by Th20, Th22; hence G1 \/ G2 = G2 by Th16; ::_thesis: G2 \/ G1 = G2 hence G2 \/ G1 = G2 by A1, Th12; ::_thesis: verum end; 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 proof let G1, G2 be Graph; ::_thesis: ( 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 ) implies G1 c= G2 ) assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( ( not G1 \/ G2 = G2 & not G2 \/ G1 = G2 ) or G1 c= G2 ) assume A2: ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) ; ::_thesis: G1 c= G2 then the carrier of G2 = the carrier of G1 \/ the carrier of G2 by A1, Def5; then A3: the carrier of G1 c= the carrier of G2 by XBOOLE_1:7; the carrier' of G2 = the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5; then A4: the carrier' of G1 c= the carrier' of G2 by XBOOLE_1:7; for v being set st v in the carrier' of G1 holds ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) proof let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) ) assume A5: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) hence A6: the Source of G1 . v = the Source of G2 . v by A1, A2, Def5; ::_thesis: ( the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) thus A7: the Target of G1 . v = the Target of G2 . v by A1, A2, A5, Def5; ::_thesis: ( the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) thus the Source of G2 . v in the carrier of G1 by A5, A6, FUNCT_2:5; ::_thesis: the Target of G2 . v in the carrier of G1 thus the Target of G2 . v in the carrier of G1 by A5, A7, FUNCT_2:5; ::_thesis: verum end; then G1 is Subgraph of G2 by A3, A4, Def18; hence G1 c= G2 by Def24; ::_thesis: verum end; theorem :: GRAPH_1:25 for G1 being Graph for G being oriented Graph st G1 c= G holds G1 is oriented proof let G1 be Graph; ::_thesis: for G being oriented Graph st G1 c= G holds G1 is oriented let G be oriented Graph; ::_thesis: ( G1 c= G implies G1 is oriented ) assume G1 c= G ; ::_thesis: G1 is oriented then A1: G1 is Subgraph of G by Def24; for x, y being set st x in the carrier' of G1 & y in the carrier' of G1 & the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y holds x = y proof let x, y be set ; ::_thesis: ( x in the carrier' of G1 & y in the carrier' of G1 & the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y implies x = y ) assume that A2: x in the carrier' of G1 and A3: y in the carrier' of G1 and A4: the Source of G1 . x = the Source of G1 . y and A5: the Target of G1 . x = the Target of G1 . y ; ::_thesis: x = y A6: the carrier' of G1 c= the carrier' of G by A1, Def18; A7: the Source of G . x = the Source of G1 . y by A1, A2, A4, Def18 .= the Source of G . y by A1, A3, Def18 ; the Target of G . x = the Target of G1 . y by A1, A2, A5, Def18 .= the Target of G . y by A1, A3, Def18 ; hence x = y by A2, A3, A6, A7, Def7; ::_thesis: verum end; hence G1 is oriented by Def7; ::_thesis: verum end; theorem :: GRAPH_1:26 for G1 being Graph for G being non-multi Graph st G1 c= G holds G1 is non-multi proof let G1 be Graph; ::_thesis: for G being non-multi Graph st G1 c= G holds G1 is non-multi let G be non-multi Graph; ::_thesis: ( G1 c= G implies G1 is non-multi ) assume G1 c= G ; ::_thesis: G1 is non-multi then A1: G1 is Subgraph of G by Def24; for x, y being set st x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) holds x = y proof let x, y be set ; ::_thesis: ( x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) implies x = y ) assume A2: ( x in the carrier' of G1 & y in the carrier' of G1 ) ; ::_thesis: ( ( not ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) & not ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) or x = y ) assume A3: ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) ; ::_thesis: x = y A4: the carrier' of G1 c= the carrier' of G by A1, Def18; A5: ( the Source of G1 . x = the Source of G . x & the Source of G1 . y = the Source of G . y ) by A1, A2, Def18; ( the Target of G1 . x = the Target of G . x & the Target of G1 . y = the Target of G . y ) by A1, A2, Def18; hence x = y by A2, A3, A4, A5, Def8; ::_thesis: verum end; hence G1 is non-multi by Def8; ::_thesis: verum end; theorem :: GRAPH_1:27 for G1 being Graph for G being simple Graph st G1 c= G holds G1 is simple proof let G1 be Graph; ::_thesis: for G being simple Graph st G1 c= G holds G1 is simple let G be simple Graph; ::_thesis: ( G1 c= G implies G1 is simple ) assume G1 c= G ; ::_thesis: G1 is simple then A1: G1 is Subgraph of G by Def24; for x being set holds ( not x in the carrier' of G1 or not the Source of G1 . x = the Target of G1 . x ) proof given x being set such that A2: x in the carrier' of G1 and A3: the Source of G1 . x = the Target of G1 . x ; ::_thesis: contradiction A4: the carrier' of G1 c= the carrier' of G by A1, Def18; the Source of G . x = the Target of G1 . x by A1, A2, A3, Def18 .= the Target of G . x by A1, A2, Def18 ; hence contradiction by A2, A4, Def9; ::_thesis: verum end; hence G1 is simple by Def9; ::_thesis: verum end; theorem :: GRAPH_1:28 for G being Graph for G1 being strict Graph holds ( G1 in bool G iff G1 c= G ) proof let G be Graph; ::_thesis: for G1 being strict Graph holds ( G1 in bool G iff G1 c= G ) let G1 be strict Graph; ::_thesis: ( G1 in bool G iff G1 c= G ) thus ( G1 in bool G implies G1 c= G ) ::_thesis: ( G1 c= G implies G1 in bool G ) proof assume G1 in bool G ; ::_thesis: G1 c= G then G1 is Subgraph of G by Def25; hence G1 c= G by Def24; ::_thesis: verum end; assume G1 c= G ; ::_thesis: G1 in bool G then G1 is Subgraph of G by Def24; hence G1 in bool G by Def25; ::_thesis: verum end; theorem Th29: :: GRAPH_1:29 for G being strict Graph holds G in bool G proof let G be strict Graph; ::_thesis: G in bool G G is Subgraph of G by Def24; hence G in bool G by Def25; ::_thesis: verum end; theorem :: GRAPH_1:30 for G2 being Graph for G1 being strict Graph holds ( G1 c= G2 iff bool G1 c= bool G2 ) proof let G2 be Graph; ::_thesis: for G1 being strict Graph holds ( G1 c= G2 iff bool G1 c= bool G2 ) let G1 be strict Graph; ::_thesis: ( G1 c= G2 iff bool G1 c= bool G2 ) thus ( G1 c= G2 implies bool G1 c= bool G2 ) ::_thesis: ( bool G1 c= bool G2 implies G1 c= G2 ) proof assume A1: G1 c= G2 ; ::_thesis: bool G1 c= bool G2 for x being set st x in bool G1 holds x in bool G2 proof let x be set ; ::_thesis: ( x in bool G1 implies x in bool G2 ) assume x in bool G1 ; ::_thesis: x in bool G2 then reconsider G = x as strict Subgraph of G1 by Def25; G c= G1 by Def24; then G c= G2 by A1, Th17; then G is strict Subgraph of G2 by Def24; hence x in bool G2 by Def25; ::_thesis: verum end; hence bool G1 c= bool G2 by TARSKI:def_3; ::_thesis: verum end; assume A2: bool G1 c= bool G2 ; ::_thesis: G1 c= G2 G1 in bool G1 by Th29; then G1 is Subgraph of G2 by A2, Def25; hence G1 c= G2 by Def24; ::_thesis: verum end; theorem :: GRAPH_1:31 for G being strict Graph holds {G} c= bool G proof let G be strict Graph; ::_thesis: {G} c= bool G G in bool G by Th29; hence {G} c= bool G by ZFMISC_1:31; ::_thesis: verum end; 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 proof let G1, G2 be strict Graph; ::_thesis: ( 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 implies G2 c= G1 ) assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( not bool (G1 \/ G2) c= (bool G1) \/ (bool G2) or G1 c= G2 or G2 c= G1 ) assume A2: bool (G1 \/ G2) c= (bool G1) \/ (bool G2) ; ::_thesis: ( G1 c= G2 or G2 c= G1 ) A3: G1 \/ G2 in bool (G1 \/ G2) by Th29; A4: now__::_thesis:_(_G1_\/_G2_in_bool_G1_implies_G2_c=_G1_) assume G1 \/ G2 in bool G1 ; ::_thesis: G2 c= G1 then G1 \/ G2 is Subgraph of G1 by Def25; then A5: G1 \/ G2 c= G1 by Def24; G1 c= G1 \/ G2 by A1, Th19; then G1 \/ G2 = G1 by A5, Th16; hence G2 c= G1 by A1, Th24; ::_thesis: verum end; now__::_thesis:_(_G1_\/_G2_in_bool_G2_implies_G1_c=_G2_) assume G1 \/ G2 in bool G2 ; ::_thesis: G1 c= G2 then G1 \/ G2 is Subgraph of G2 by Def25; then A6: G1 \/ G2 c= G2 by Def24; G2 c= G1 \/ G2 by A1, Th19; then G1 \/ G2 = G2 by A6, Th16; hence G1 c= G2 by A1, Th24; ::_thesis: verum end; hence ( G1 c= G2 or G2 c= G1 ) by A2, A3, A4, XBOOLE_0:def_3; ::_thesis: verum end; 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) proof let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies (bool G1) \/ (bool G2) c= bool (G1 \/ G2) ) assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: (bool G1) \/ (bool G2) c= bool (G1 \/ G2) A2: for v being set st v in bool G1 holds v in bool (G1 \/ G2) proof let v be set ; ::_thesis: ( v in bool G1 implies v in bool (G1 \/ G2) ) assume v in bool G1 ; ::_thesis: v in bool (G1 \/ G2) then reconsider G = v as strict Subgraph of G1 by Def25; ( G c= G1 & G1 c= G1 \/ G2 ) by A1, Def24, Th19; then G c= G1 \/ G2 by Th17; then G is strict Subgraph of G1 \/ G2 by Def24; hence v in bool (G1 \/ G2) by Def25; ::_thesis: verum end; A3: for v being set st v in bool G2 holds v in bool (G1 \/ G2) proof let v be set ; ::_thesis: ( v in bool G2 implies v in bool (G1 \/ G2) ) assume v in bool G2 ; ::_thesis: v in bool (G1 \/ G2) then reconsider G = v as strict Subgraph of G2 by Def25; ( G c= G2 & G2 c= G1 \/ G2 ) by A1, Def24, Th19; then G c= G1 \/ G2 by Th17; then G is strict Subgraph of G1 \/ G2 by Def24; hence v in bool (G1 \/ G2) by Def25; ::_thesis: verum end; for v being set st v in (bool G1) \/ (bool G2) holds v in bool (G1 \/ G2) proof let v be set ; ::_thesis: ( v in (bool G1) \/ (bool G2) implies v in bool (G1 \/ G2) ) assume v in (bool G1) \/ (bool G2) ; ::_thesis: v in bool (G1 \/ G2) then ( v in bool G1 or v in bool G2 ) by XBOOLE_0:def_3; hence v in bool (G1 \/ G2) by A2, A3; ::_thesis: verum end; hence (bool G1) \/ (bool G2) c= bool (G1 \/ G2) by TARSKI:def_3; ::_thesis: verum end; 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 proof let G1, G, G2 be Graph; ::_thesis: ( G1 in bool G & G2 in bool G implies G1 \/ G2 in bool G ) assume that A1: G1 in bool G and A2: G2 in bool G ; ::_thesis: G1 \/ G2 in bool G A3: G1 is Subgraph of G by A1, Def25; A4: G2 is Subgraph of G by A2, Def25; A5: G1 c= G by A3, Def24; G2 c= G by A4, Def24; then G1 \/ G2 c= G by A5, Th22; then G1 \/ G2 is Subgraph of G by Def24; hence G1 \/ G2 in bool G by Def25; ::_thesis: verum end;