:: GLIB_000 semantic presentation begin registration cluster Relation-like NAT -defined Function-like finite for set ; existence ex b1 being Function st ( b1 is finite & b1 is NAT -defined ) proof take {} ; ::_thesis: ( {} is finite & {} is NAT -defined ) thus {} is finite ; ::_thesis: {} is NAT -defined thus dom {} c= NAT ; :: according to RELAT_1:def_18 ::_thesis: verum end; end; definition mode GraphStruct is NAT -defined finite Function; end; definition func VertexSelector -> Element of NAT equals :: GLIB_000:def 1 1; coherence 1 is Element of NAT ; func EdgeSelector -> Element of NAT equals :: GLIB_000:def 2 2; coherence 2 is Element of NAT ; func SourceSelector -> Element of NAT equals :: GLIB_000:def 3 3; coherence 3 is Element of NAT ; func TargetSelector -> Element of NAT equals :: GLIB_000:def 4 4; coherence 4 is Element of NAT ; end; :: deftheorem defines VertexSelector GLIB_000:def_1_:_ VertexSelector = 1; :: deftheorem defines EdgeSelector GLIB_000:def_2_:_ EdgeSelector = 2; :: deftheorem defines SourceSelector GLIB_000:def_3_:_ SourceSelector = 3; :: deftheorem defines TargetSelector GLIB_000:def_4_:_ TargetSelector = 4; definition func _GraphSelectors -> non empty Subset of NAT equals :: GLIB_000:def 5 {VertexSelector,EdgeSelector,SourceSelector,TargetSelector}; coherence {VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty Subset of NAT ; end; :: deftheorem defines _GraphSelectors GLIB_000:def_5_:_ _GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector}; definition let G be GraphStruct; func the_Vertices_of G -> set equals :: GLIB_000:def 6 G . VertexSelector; coherence G . VertexSelector is set ; func the_Edges_of G -> set equals :: GLIB_000:def 7 G . EdgeSelector; coherence G . EdgeSelector is set ; func the_Source_of G -> set equals :: GLIB_000:def 8 G . SourceSelector; coherence G . SourceSelector is set ; func the_Target_of G -> set equals :: GLIB_000:def 9 G . TargetSelector; coherence G . TargetSelector is set ; end; :: deftheorem defines the_Vertices_of GLIB_000:def_6_:_ for G being GraphStruct holds the_Vertices_of G = G . VertexSelector; :: deftheorem defines the_Edges_of GLIB_000:def_7_:_ for G being GraphStruct holds the_Edges_of G = G . EdgeSelector; :: deftheorem defines the_Source_of GLIB_000:def_8_:_ for G being GraphStruct holds the_Source_of G = G . SourceSelector; :: deftheorem defines the_Target_of GLIB_000:def_9_:_ for G being GraphStruct holds the_Target_of G = G . TargetSelector; definition let G be GraphStruct; attrG is [Graph-like] means :Def10: :: GLIB_000:def 10 ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) & the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) ); end; :: deftheorem Def10 defines [Graph-like] GLIB_000:def_10_:_ for G being GraphStruct holds ( G is [Graph-like] iff ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) & the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) ) ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] for set ; existence ex b1 being GraphStruct st b1 is [Graph-like] proof set V = {1}; set E = {} ; reconsider S = {} as Function of {},{1} by RELSET_1:12; set G = <*{1},{},S,S*>; len <*{1},{},S,S*> = 4 by FINSEQ_4:76; then A1: dom <*{1},{},S,S*> = Seg 4 by FINSEQ_1:def_3; reconsider G = <*{1},{},S,S*> as GraphStruct ; A2: ( SourceSelector in dom G & TargetSelector in dom G ) by A1, FINSEQ_1:1; A3: ( the_Vertices_of G = {1} & the_Edges_of G = {} ) by FINSEQ_4:76; A4: ( the_Source_of G = S & the_Target_of G = S ) by FINSEQ_4:76; ( VertexSelector in dom G & EdgeSelector in dom G ) by A1, FINSEQ_1:1; then G is [Graph-like] by A3, A4, A2, Def10; hence ex b1 being GraphStruct st b1 is [Graph-like] ; ::_thesis: verum end; end; definition mode _Graph is [Graph-like] GraphStruct; end; registration let G be _Graph; cluster the_Vertices_of G -> non empty ; coherence not the_Vertices_of G is empty by Def10; end; definition let G be _Graph; :: original: the_Source_of redefine func the_Source_of G -> Function of (the_Edges_of G),(the_Vertices_of G); coherence the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10; :: original: the_Target_of redefine func the_Target_of G -> Function of (the_Edges_of G),(the_Vertices_of G); coherence the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10; end; definition let V be non empty set ; let E be set ; let S, T be Function of E,V; func createGraph (V,E,S,T) -> _Graph equals :: GLIB_000:def 11 <*V,E,S,T*>; coherence <*V,E,S,T*> is _Graph proof set G = <*V,E,S,T*>; len <*V,E,S,T*> = 4 by FINSEQ_4:76; then A1: dom <*V,E,S,T*> = Seg 4 by FINSEQ_1:def_3; reconsider G = <*V,E,S,T*> as GraphStruct ; A2: ( SourceSelector in dom G & TargetSelector in dom G ) by A1, FINSEQ_1:1; A3: ( the_Vertices_of G = V & the_Edges_of G = E ) by FINSEQ_4:76; A4: ( the_Source_of G = S & the_Target_of G = T ) by FINSEQ_4:76; ( VertexSelector in dom G & EdgeSelector in dom G ) by A1, FINSEQ_1:1; hence <*V,E,S,T*> is _Graph by A3, A4, A2, Def10; ::_thesis: verum end; end; :: deftheorem defines createGraph GLIB_000:def_11_:_ for V being non empty set for E being set for S, T being Function of E,V holds createGraph (V,E,S,T) = <*V,E,S,T*>; definition let G be GraphStruct; let n be Nat; let x be set ; funcG .set (n,x) -> GraphStruct equals :: GLIB_000:def 12 G +* (n .--> x); coherence G +* (n .--> x) is GraphStruct proof set IT = G +* (n .--> x); A1: dom (n .--> x) = {n} by FUNCOP_1:13; n in NAT by ORDINAL1:def_12; then A2: {n} c= NAT by ZFMISC_1:31; ( dom (G +* (n .--> x)) = (dom G) \/ (dom (n .--> x)) & dom G c= NAT ) by FUNCT_4:def_1; then dom (G +* (n .--> x)) c= NAT by A2, A1, XBOOLE_1:8; hence G +* (n .--> x) is GraphStruct by RELAT_1:def_18; ::_thesis: verum end; end; :: deftheorem defines .set GLIB_000:def_12_:_ for G being GraphStruct for n being Nat for x being set holds G .set (n,x) = G +* (n .--> x); Lm1: for GS being GraphStruct holds ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) proof let GS be GraphStruct; ::_thesis: ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) now__::_thesis:_(_(_VertexSelector_in_dom_GS_&_EdgeSelector_in_dom_GS_&_SourceSelector_in_dom_GS_&_TargetSelector_in_dom_GS_implies__GraphSelectors_c=_dom_GS_)_&_(__GraphSelectors_c=_dom_GS_implies_(_VertexSelector_in_dom_GS_&_EdgeSelector_in_dom_GS_&_SourceSelector_in_dom_GS_&_TargetSelector_in_dom_GS_)_)_) hereby ::_thesis: ( _GraphSelectors c= dom GS implies ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) ) assume ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) ; ::_thesis: _GraphSelectors c= dom GS then for x being set st x in _GraphSelectors holds x in dom GS by ENUMSET1:def_2; hence _GraphSelectors c= dom GS by TARSKI:def_3; ::_thesis: verum end; A1: ( VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors ) by ENUMSET1:def_2; A2: ( SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors ) by ENUMSET1:def_2; assume _GraphSelectors c= dom GS ; ::_thesis: ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) hence ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) by A1, A2; ::_thesis: verum end; hence ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) by Def10; ::_thesis: verum end; registration let G be _Graph; clusterG | _GraphSelectors -> [Graph-like] ; coherence G | _GraphSelectors is [Graph-like] proof now__::_thesis:_for_x_being_set_st_x_in__GraphSelectors_holds_ x_in_dom_G let x be set ; ::_thesis: ( x in _GraphSelectors implies x in dom G ) assume x in _GraphSelectors ; ::_thesis: x in dom G then ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector ) by ENUMSET1:def_2; hence x in dom G by Def10; ::_thesis: verum end; then A1: _GraphSelectors c= dom G by TARSKI:def_3; set G2 = G | _GraphSelectors; VertexSelector in _GraphSelectors by ENUMSET1:def_2; then A2: the_Vertices_of (G | _GraphSelectors) = the_Vertices_of G by FUNCT_1:49; EdgeSelector in _GraphSelectors by ENUMSET1:def_2; then A3: the_Edges_of (G | _GraphSelectors) = the_Edges_of G by FUNCT_1:49; TargetSelector in _GraphSelectors by ENUMSET1:def_2; then A4: the_Target_of (G | _GraphSelectors) = the_Target_of G by FUNCT_1:49; SourceSelector in _GraphSelectors by ENUMSET1:def_2; then A5: the_Source_of (G | _GraphSelectors) = the_Source_of G by FUNCT_1:49; dom (G | _GraphSelectors) = (dom G) /\ _GraphSelectors by RELAT_1:61 .= _GraphSelectors by A1, XBOOLE_1:28 ; hence G | _GraphSelectors is [Graph-like] by A2, A3, A5, A4, Lm1; ::_thesis: verum end; end; definition let G be _Graph; let x, y, e be set ; prede Joins x,y,G means :Def13: :: GLIB_000:def 13 ( e in the_Edges_of G & ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) ); end; :: deftheorem Def13 defines Joins GLIB_000:def_13_:_ for G being _Graph for x, y, e being set holds ( e Joins x,y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) ) ); definition let G be _Graph; let x, y, e be set ; prede DJoins x,y,G means :Def14: :: GLIB_000:def 14 ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ); end; :: deftheorem Def14 defines DJoins GLIB_000:def_14_:_ for G being _Graph for x, y, e being set holds ( e DJoins x,y,G iff ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ) ); definition let G be _Graph; let X, Y, e be set ; prede SJoins X,Y,G means :Def15: :: GLIB_000:def 15 ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ); prede DSJoins X,Y,G means :Def16: :: GLIB_000:def 16 ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ); end; :: deftheorem Def15 defines SJoins GLIB_000:def_15_:_ for G being _Graph for X, Y, e being set holds ( e SJoins X,Y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ) ); :: deftheorem Def16 defines DSJoins GLIB_000:def_16_:_ for G being _Graph for X, Y, e being set holds ( e DSJoins X,Y,G iff ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) ); Lm2: for G being _Graph for e, x, y being set holds ( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) proof let G be _Graph; ::_thesis: for e, x, y being set holds ( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) let e, x, y be set ; ::_thesis: ( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) hereby ::_thesis: ( ( e DJoins x,y,G or e DJoins y,x,G ) implies e Joins x,y,G ) assume A1: e Joins x,y,G ; ::_thesis: ( e DJoins x,y,G or e DJoins y,x,G ) then A2: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by Def13; e in the_Edges_of G by A1, Def13; hence ( e DJoins x,y,G or e DJoins y,x,G ) by A2, Def14; ::_thesis: verum end; assume A3: ( e DJoins x,y,G or e DJoins y,x,G ) ; ::_thesis: e Joins x,y,G then A4: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by Def14; e in the_Edges_of G by A3, Def14; hence e Joins x,y,G by A4, Def13; ::_thesis: verum end; definition let G be _Graph; attrG is finite means :Def17: :: GLIB_000:def 17 ( the_Vertices_of G is finite & the_Edges_of G is finite ); attrG is loopless means :Def18: :: GLIB_000:def 18 for e being set holds ( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ); attrG is trivial means :Def19: :: GLIB_000:def 19 card (the_Vertices_of G) = 1; attrG is non-multi means :Def20: :: GLIB_000:def 20 for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds e1 = e2; attrG is non-Dmulti means :Def21: :: GLIB_000:def 21 for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds e1 = e2; end; :: deftheorem Def17 defines finite GLIB_000:def_17_:_ for G being _Graph holds ( G is finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) ); :: deftheorem Def18 defines loopless GLIB_000:def_18_:_ for G being _Graph holds ( G is loopless iff for e being set holds ( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) ); :: deftheorem Def19 defines trivial GLIB_000:def_19_:_ for G being _Graph holds ( G is trivial iff card (the_Vertices_of G) = 1 ); :: deftheorem Def20 defines non-multi GLIB_000:def_20_:_ for G being _Graph holds ( G is non-multi iff for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds e1 = e2 ); :: deftheorem Def21 defines non-Dmulti GLIB_000:def_21_:_ for G being _Graph holds ( G is non-Dmulti iff for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds e1 = e2 ); definition let G be _Graph; attrG is simple means :Def22: :: GLIB_000:def 22 ( G is loopless & G is non-multi ); attrG is Dsimple means :Def23: :: GLIB_000:def 23 ( G is loopless & G is non-Dmulti ); end; :: deftheorem Def22 defines simple GLIB_000:def_22_:_ for G being _Graph holds ( G is simple iff ( G is loopless & G is non-multi ) ); :: deftheorem Def23 defines Dsimple GLIB_000:def_23_:_ for G being _Graph holds ( G is Dsimple iff ( G is loopless & G is non-Dmulti ) ); Lm3: for G being _Graph st the_Edges_of G = {} holds G is simple proof let G be _Graph; ::_thesis: ( the_Edges_of G = {} implies G is simple ) assume A1: the_Edges_of G = {} ; ::_thesis: G is simple then for e being set holds ( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) ; then A2: G is loopless by Def18; for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds e1 = e2 by A1, Def13; then G is non-multi by Def20; hence G is simple by A2, Def22; ::_thesis: verum end; registration cluster Relation-like NAT -defined Function-like finite [Graph-like] non-multi -> non-Dmulti for set ; coherence for b1 being _Graph st b1 is non-multi holds b1 is non-Dmulti proof let G be _Graph; ::_thesis: ( G is non-multi implies G is non-Dmulti ) assume A1: G is non-multi ; ::_thesis: G is non-Dmulti now__::_thesis:_for_e1,_e2,_v1,_v2_being_set_st_e1_DJoins_v1,v2,G_&_e2_DJoins_v1,v2,G_holds_ e1_=_e2 let e1, e2, v1, v2 be set ; ::_thesis: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2 ) assume ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; ::_thesis: e1 = e2 then ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by Lm2; hence e1 = e2 by A1, Def20; ::_thesis: verum end; hence G is non-Dmulti by Def21; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like finite [Graph-like] simple -> loopless non-multi for set ; coherence for b1 being _Graph st b1 is simple holds ( b1 is loopless & b1 is non-multi ) by Def22; cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-multi -> simple for set ; coherence for b1 being _Graph st b1 is loopless & b1 is non-multi holds b1 is simple by Def22; cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-Dmulti -> Dsimple for set ; coherence for b1 being _Graph st b1 is loopless & b1 is non-Dmulti holds b1 is Dsimple by Def23; cluster Relation-like NAT -defined Function-like finite [Graph-like] Dsimple -> loopless non-Dmulti for set ; coherence for b1 being _Graph st b1 is Dsimple holds ( b1 is loopless & b1 is non-Dmulti ) by Def23; cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless trivial -> finite for set ; coherence for b1 being _Graph st b1 is trivial & b1 is loopless holds b1 is finite proof let G be _Graph; ::_thesis: ( G is trivial & G is loopless implies G is finite ) assume that A2: G is trivial and A3: G is loopless ; ::_thesis: G is finite card (the_Vertices_of G) = 1 by A2, Def19; then consider v being set such that A4: the_Vertices_of G = {v} by CARD_2:42; now__::_thesis:_the_Edges_of_G_is_finite percases ( the_Edges_of G is empty or not the_Edges_of G is empty ) ; suppose the_Edges_of G is empty ; ::_thesis: the_Edges_of G is finite hence the_Edges_of G is finite ; ::_thesis: verum end; suppose not the_Edges_of G is empty ; ::_thesis: the_Edges_of G is finite then consider e being set such that A5: e in the_Edges_of G by XBOOLE_0:def_1; (the_Target_of G) . e in the_Vertices_of G by A5, FUNCT_2:5; then A6: (the_Target_of G) . e = v by A4, TARSKI:def_1; (the_Source_of G) . e in the_Vertices_of G by A5, FUNCT_2:5; then (the_Source_of G) . e = v by A4, TARSKI:def_1; hence the_Edges_of G is finite by A3, A5, A6, Def18; ::_thesis: verum end; end; end; hence G is finite by A4, Def17; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial non-Dmulti -> finite for set ; coherence for b1 being _Graph st b1 is trivial & b1 is non-Dmulti holds b1 is finite proof let G be _Graph; ::_thesis: ( G is trivial & G is non-Dmulti implies G is finite ) assume that A7: G is trivial and A8: G is non-Dmulti ; ::_thesis: G is finite card (the_Vertices_of G) = 1 by A7, Def19; then consider v being set such that A9: the_Vertices_of G = {v} by CARD_2:42; now__::_thesis:_the_Edges_of_G_is_finite set e1 = choose (the_Edges_of G); set v1 = (the_Source_of G) . (choose (the_Edges_of G)); set v2 = (the_Target_of G) . (choose (the_Edges_of G)); assume A10: not the_Edges_of G is finite ; ::_thesis: contradiction then A11: the_Edges_of G <> {} ; (the_Target_of G) . (choose (the_Edges_of G)) in the_Vertices_of G by A10, FUNCT_2:5; then A12: (the_Target_of G) . (choose (the_Edges_of G)) = v by A9, TARSKI:def_1; (the_Source_of G) . (choose (the_Edges_of G)) in the_Vertices_of G by A10, FUNCT_2:5; then (the_Source_of G) . (choose (the_Edges_of G)) = v by A9, TARSKI:def_1; then A13: choose (the_Edges_of G) DJoins v,v,G by A11, A12, Def14; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_{(choose_(the_Edges_of_G))}_implies_x_in_the_Edges_of_G_)_&_(_x_in_the_Edges_of_G_implies_x_in_{(choose_(the_Edges_of_G))}_)_) let x be set ; ::_thesis: ( ( x in {(choose (the_Edges_of G))} implies x in the_Edges_of G ) & ( x in the_Edges_of G implies x in {(choose (the_Edges_of G))} ) ) set v1 = (the_Source_of G) . x; set v2 = (the_Target_of G) . x; hereby ::_thesis: ( x in the_Edges_of G implies x in {(choose (the_Edges_of G))} ) assume x in {(choose (the_Edges_of G))} ; ::_thesis: x in the_Edges_of G then x = choose (the_Edges_of G) by TARSKI:def_1; hence x in the_Edges_of G by A11; ::_thesis: verum end; assume A14: x in the_Edges_of G ; ::_thesis: x in {(choose (the_Edges_of G))} then (the_Target_of G) . x in the_Vertices_of G by FUNCT_2:5; then A15: (the_Target_of G) . x = v by A9, TARSKI:def_1; (the_Source_of G) . x in the_Vertices_of G by A14, FUNCT_2:5; then (the_Source_of G) . x = v by A9, TARSKI:def_1; then x DJoins v,v,G by A14, A15, Def14; then x = choose (the_Edges_of G) by A8, A13, Def21; hence x in {(choose (the_Edges_of G))} by TARSKI:def_1; ::_thesis: verum end; hence contradiction by A10, TARSKI:1; ::_thesis: verum end; hence G is finite by A9, Def17; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple for set ; existence ex b1 being _Graph st ( b1 is trivial & b1 is simple ) proof set V = {1}; set E = {} ; reconsider S = {} as Function of {},{1} by RELSET_1:12; set G = createGraph ({1},{},S,S); take createGraph ({1},{},S,S) ; ::_thesis: ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is simple ) the_Vertices_of (createGraph ({1},{},S,S)) = {1} by FINSEQ_4:76; then card (the_Vertices_of (createGraph ({1},{},S,S))) = 1 by CARD_1:30; hence createGraph ({1},{},S,S) is trivial by Def19; ::_thesis: createGraph ({1},{},S,S) is simple the_Edges_of (createGraph ({1},{},S,S)) = {} by FINSEQ_4:76; then for e1, e2, v1, v2 being set st e1 Joins v1,v2, createGraph ({1},{},S,S) & e2 Joins v1,v2, createGraph ({1},{},S,S) holds e1 = e2 by Def13; then A1: createGraph ({1},{},S,S) is non-multi by Def20; for e being set holds ( not e in the_Edges_of (createGraph ({1},{},S,S)) or not (the_Source_of (createGraph ({1},{},S,S))) . e = (the_Target_of (createGraph ({1},{},S,S))) . e ) by FINSEQ_4:76; then createGraph ({1},{},S,S) is loopless by Def18; hence createGraph ({1},{},S,S) is simple by A1; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial simple for set ; existence ex b1 being _Graph st ( b1 is finite & not b1 is trivial & b1 is simple ) proof set V = {1,2}; set E = {} ; reconsider S = {} as Function of {},{1,2} by RELSET_1:12; set G = createGraph ({1,2},{},S,S); take createGraph ({1,2},{},S,S) ; ::_thesis: ( createGraph ({1,2},{},S,S) is finite & not createGraph ({1,2},{},S,S) is trivial & createGraph ({1,2},{},S,S) is simple ) A2: the_Edges_of (createGraph ({1,2},{},S,S)) = {} by FINSEQ_4:76; A3: the_Vertices_of (createGraph ({1,2},{},S,S)) = {1,2} by FINSEQ_4:76; hence createGraph ({1,2},{},S,S) is finite by A2, Def17; ::_thesis: ( not createGraph ({1,2},{},S,S) is trivial & createGraph ({1,2},{},S,S) is simple ) card (the_Vertices_of (createGraph ({1,2},{},S,S))) <> 1 by A3, CARD_2:57; hence not createGraph ({1,2},{},S,S) is trivial by Def19; ::_thesis: createGraph ({1,2},{},S,S) is simple for e being set holds ( not e in the_Edges_of (createGraph ({1,2},{},S,S)) or not (the_Source_of (createGraph ({1,2},{},S,S))) . e = (the_Target_of (createGraph ({1,2},{},S,S))) . e ) by FINSEQ_4:76; then A4: createGraph ({1,2},{},S,S) is loopless by Def18; for e1, e2, v1, v2 being set st e1 Joins v1,v2, createGraph ({1,2},{},S,S) & e2 Joins v1,v2, createGraph ({1,2},{},S,S) holds e1 = e2 by A2, Def13; then createGraph ({1,2},{},S,S) is non-multi by Def20; hence createGraph ({1,2},{},S,S) is simple by A4; ::_thesis: verum end; end; registration let G be finite _Graph; cluster the_Vertices_of G -> finite ; coherence the_Vertices_of G is finite by Def17; cluster the_Edges_of G -> finite ; coherence the_Edges_of G is finite by Def17; end; registration let G be trivial _Graph; cluster the_Vertices_of G -> finite ; coherence the_Vertices_of G is finite proof card (the_Vertices_of G) = 1 by Def19; hence the_Vertices_of G is finite ; ::_thesis: verum end; end; registration let V be non empty finite set ; let E be finite set ; let S, T be Function of E,V; cluster createGraph (V,E,S,T) -> finite ; coherence createGraph (V,E,S,T) is finite proof set G = createGraph (V,E,S,T); ( the_Vertices_of (createGraph (V,E,S,T)) = V & the_Edges_of (createGraph (V,E,S,T)) = E ) by FINSEQ_4:76; hence createGraph (V,E,S,T) is finite by Def17; ::_thesis: verum end; end; registration let V be non empty set ; let E be empty set ; let S, T be Function of E,V; cluster createGraph (V,E,S,T) -> simple ; coherence createGraph (V,E,S,T) is simple proof set G = createGraph (V,E,S,T); the_Edges_of (createGraph (V,E,S,T)) = E by FINSEQ_4:76; then for e1, e2, v1, v2 being set st e1 Joins v1,v2, createGraph (V,E,S,T) & e2 Joins v1,v2, createGraph (V,E,S,T) holds e1 = e2 by Def13; then A1: createGraph (V,E,S,T) is non-multi by Def20; for e being set holds ( not e in the_Edges_of (createGraph (V,E,S,T)) or not (the_Source_of (createGraph (V,E,S,T))) . e = (the_Target_of (createGraph (V,E,S,T))) . e ) by FINSEQ_4:76; then createGraph (V,E,S,T) is loopless by Def18; hence createGraph (V,E,S,T) is simple by A1; ::_thesis: verum end; end; registration let v, E be set ; let S, T be Function of E,{v}; cluster createGraph ({v},E,S,T) -> trivial ; coherence createGraph ({v},E,S,T) is trivial proof set G = createGraph ({v},E,S,T); the_Vertices_of (createGraph ({v},E,S,T)) = {v} by FINSEQ_4:76; then card (the_Vertices_of (createGraph ({v},E,S,T))) = 1 by CARD_1:30; hence createGraph ({v},E,S,T) is trivial by Def19; ::_thesis: verum end; end; definition let G be _Graph; funcG .order() -> Cardinal equals :: GLIB_000:def 24 card (the_Vertices_of G); coherence card (the_Vertices_of G) is Cardinal ; end; :: deftheorem defines .order() GLIB_000:def_24_:_ for G being _Graph holds G .order() = card (the_Vertices_of G); definition let G be finite _Graph; :: original: .order() redefine funcG .order() -> non empty Element of NAT ; coherence G .order() is non empty Element of NAT proof G .order() = card (the_Vertices_of G) ; hence G .order() is non empty Element of NAT ; ::_thesis: verum end; end; definition let G be _Graph; funcG .size() -> Cardinal equals :: GLIB_000:def 25 card (the_Edges_of G); coherence card (the_Edges_of G) is Cardinal ; end; :: deftheorem defines .size() GLIB_000:def_25_:_ for G being _Graph holds G .size() = card (the_Edges_of G); definition let G be finite _Graph; :: original: .size() redefine funcG .size() -> Element of NAT ; coherence G .size() is Element of NAT proof G .size() = card (the_Edges_of G) ; hence G .size() is Element of NAT ; ::_thesis: verum end; end; definition let G be _Graph; let X be set ; funcG .edgesInto X -> Subset of (the_Edges_of G) means :Def26: :: GLIB_000:def 26 for e being set holds ( e in it iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ); existence ex b1 being Subset of (the_Edges_of G) st for e being set holds ( e in b1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) proof defpred S1[ set ] means (the_Target_of G) . $1 in X; consider IT being Subset of (the_Edges_of G) such that A1: for e being set holds ( e in IT iff ( e in the_Edges_of G & S1[e] ) ) from SUBSET_1:sch_1(); take IT ; ::_thesis: for e being set holds ( e in IT iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) thus for e being set holds ( e in IT iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds ( e in b1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) & ( for e being set holds ( e in b2 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) holds b1 = b2 proof let IT1, IT2 be Subset of (the_Edges_of G); ::_thesis: ( ( for e being set holds ( e in IT1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) & ( for e being set holds ( e in IT2 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) implies IT1 = IT2 ) assume that A2: for e being set holds ( e in IT1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) and A3: for e being set holds ( e in IT2 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_e_being_set_holds_ (_(_e_in_IT1_implies_e_in_IT2_)_&_(_e_in_IT2_implies_e_in_IT1_)_) let e be set ; ::_thesis: ( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) ) hereby ::_thesis: ( e in IT2 implies e in IT1 ) assume A4: e in IT1 ; ::_thesis: e in IT2 then (the_Target_of G) . e in X by A2; hence e in IT2 by A3, A4; ::_thesis: verum end; assume A5: e in IT2 ; ::_thesis: e in IT1 then (the_Target_of G) . e in X by A3; hence e in IT1 by A2, A5; ::_thesis: verum end; hence IT1 = IT2 by TARSKI:1; ::_thesis: verum end; funcG .edgesOutOf X -> Subset of (the_Edges_of G) means :Def27: :: GLIB_000:def 27 for e being set holds ( e in it iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ); existence ex b1 being Subset of (the_Edges_of G) st for e being set holds ( e in b1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) proof defpred S1[ set ] means (the_Source_of G) . $1 in X; consider IT being Subset of (the_Edges_of G) such that A6: for e being set holds ( e in IT iff ( e in the_Edges_of G & S1[e] ) ) from SUBSET_1:sch_1(); take IT ; ::_thesis: for e being set holds ( e in IT iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) thus for e being set holds ( e in IT iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds ( e in b1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds ( e in b2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) holds b1 = b2 proof let IT1, IT2 be Subset of (the_Edges_of G); ::_thesis: ( ( for e being set holds ( e in IT1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds ( e in IT2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) implies IT1 = IT2 ) assume that A7: for e being set holds ( e in IT1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) and A8: for e being set holds ( e in IT2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_e_being_set_holds_ (_(_e_in_IT1_implies_e_in_IT2_)_&_(_e_in_IT2_implies_e_in_IT1_)_) let e be set ; ::_thesis: ( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) ) hereby ::_thesis: ( e in IT2 implies e in IT1 ) assume A9: e in IT1 ; ::_thesis: e in IT2 then (the_Source_of G) . e in X by A7; hence e in IT2 by A8, A9; ::_thesis: verum end; assume A10: e in IT2 ; ::_thesis: e in IT1 then (the_Source_of G) . e in X by A8; hence e in IT1 by A7, A10; ::_thesis: verum end; hence IT1 = IT2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def26 defines .edgesInto GLIB_000:def_26_:_ for G being _Graph for X being set for b3 being Subset of (the_Edges_of G) holds ( b3 = G .edgesInto X iff for e being set holds ( e in b3 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ); :: deftheorem Def27 defines .edgesOutOf GLIB_000:def_27_:_ for G being _Graph for X being set for b3 being Subset of (the_Edges_of G) holds ( b3 = G .edgesOutOf X iff for e being set holds ( e in b3 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ); definition let G be _Graph; let X be set ; funcG .edgesInOut X -> Subset of (the_Edges_of G) equals :: GLIB_000:def 28 (G .edgesInto X) \/ (G .edgesOutOf X); coherence (G .edgesInto X) \/ (G .edgesOutOf X) is Subset of (the_Edges_of G) ; funcG .edgesBetween X -> Subset of (the_Edges_of G) equals :: GLIB_000:def 29 (G .edgesInto X) /\ (G .edgesOutOf X); coherence (G .edgesInto X) /\ (G .edgesOutOf X) is Subset of (the_Edges_of G) ; end; :: deftheorem defines .edgesInOut GLIB_000:def_28_:_ for G being _Graph for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X); :: deftheorem defines .edgesBetween GLIB_000:def_29_:_ for G being _Graph for X being set holds G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X); definition let G be _Graph; let X, Y be set ; funcG .edgesBetween (X,Y) -> Subset of (the_Edges_of G) means :Def30: :: GLIB_000:def 30 for e being set holds ( e in it iff e SJoins X,Y,G ); existence ex b1 being Subset of (the_Edges_of G) st for e being set holds ( e in b1 iff e SJoins X,Y,G ) proof defpred S1[ set ] means $1 SJoins X,Y,G; consider IT being Subset of (the_Edges_of G) such that A1: for e being set holds ( e in IT iff ( e in the_Edges_of G & S1[e] ) ) from SUBSET_1:sch_1(); take IT ; ::_thesis: for e being set holds ( e in IT iff e SJoins X,Y,G ) let e be set ; ::_thesis: ( e in IT iff e SJoins X,Y,G ) thus ( e in IT implies S1[e] ) by A1; ::_thesis: ( e SJoins X,Y,G implies e in IT ) assume A2: e SJoins X,Y,G ; ::_thesis: e in IT then e in the_Edges_of G by Def15; hence e in IT by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds ( e in b1 iff e SJoins X,Y,G ) ) & ( for e being set holds ( e in b2 iff e SJoins X,Y,G ) ) holds b1 = b2 proof let IT1, IT2 be Subset of (the_Edges_of G); ::_thesis: ( ( for e being set holds ( e in IT1 iff e SJoins X,Y,G ) ) & ( for e being set holds ( e in IT2 iff e SJoins X,Y,G ) ) implies IT1 = IT2 ) assume that A3: for e being set holds ( e in IT1 iff e SJoins X,Y,G ) and A4: for e being set holds ( e in IT2 iff e SJoins X,Y,G ) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_e_being_set_holds_ (_e_in_IT2_iff_e_in_IT1_) let e be set ; ::_thesis: ( e in IT2 iff e in IT1 ) ( e in IT1 iff e SJoins X,Y,G ) by A3; hence ( e in IT2 iff e in IT1 ) by A4; ::_thesis: verum end; hence IT1 = IT2 by TARSKI:1; ::_thesis: verum end; funcG .edgesDBetween (X,Y) -> Subset of (the_Edges_of G) means :Def31: :: GLIB_000:def 31 for e being set holds ( e in it iff e DSJoins X,Y,G ); existence ex b1 being Subset of (the_Edges_of G) st for e being set holds ( e in b1 iff e DSJoins X,Y,G ) proof defpred S1[ set ] means $1 DSJoins X,Y,G; consider IT being Subset of (the_Edges_of G) such that A5: for e being set holds ( e in IT iff ( e in the_Edges_of G & S1[e] ) ) from SUBSET_1:sch_1(); take IT ; ::_thesis: for e being set holds ( e in IT iff e DSJoins X,Y,G ) let e be set ; ::_thesis: ( e in IT iff e DSJoins X,Y,G ) thus ( e in IT implies S1[e] ) by A5; ::_thesis: ( e DSJoins X,Y,G implies e in IT ) assume A6: e DSJoins X,Y,G ; ::_thesis: e in IT then e in the_Edges_of G by Def16; hence e in IT by A5, A6; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds ( e in b1 iff e DSJoins X,Y,G ) ) & ( for e being set holds ( e in b2 iff e DSJoins X,Y,G ) ) holds b1 = b2 proof let IT1, IT2 be Subset of (the_Edges_of G); ::_thesis: ( ( for e being set holds ( e in IT1 iff e DSJoins X,Y,G ) ) & ( for e being set holds ( e in IT2 iff e DSJoins X,Y,G ) ) implies IT1 = IT2 ) assume that A7: for e being set holds ( e in IT1 iff e DSJoins X,Y,G ) and A8: for e being set holds ( e in IT2 iff e DSJoins X,Y,G ) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_e_being_set_holds_ (_e_in_IT2_iff_e_in_IT1_) let e be set ; ::_thesis: ( e in IT2 iff e in IT1 ) ( e in IT1 iff e DSJoins X,Y,G ) by A7; hence ( e in IT2 iff e in IT1 ) by A8; ::_thesis: verum end; hence IT1 = IT2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def30 defines .edgesBetween GLIB_000:def_30_:_ for G being _Graph for X, Y being set for b4 being Subset of (the_Edges_of G) holds ( b4 = G .edgesBetween (X,Y) iff for e being set holds ( e in b4 iff e SJoins X,Y,G ) ); :: deftheorem Def31 defines .edgesDBetween GLIB_000:def_31_:_ for G being _Graph for X, Y being set for b4 being Subset of (the_Edges_of G) holds ( b4 = G .edgesDBetween (X,Y) iff for e being set holds ( e in b4 iff e DSJoins X,Y,G ) ); scheme :: GLIB_000:sch 1 FinGraphOrderInd{ P1[ finite _Graph] } : for G being finite _Graph holds P1[G] provided A1: for G being finite _Graph st G .order() = 1 holds P1[G] and A2: for k being non empty Nat st ( for Gk being finite _Graph st Gk .order() = k holds P1[Gk] ) holds for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds P1[Gk1] proof defpred S1[ Nat] means for G being finite _Graph st G .order() = $1 holds P1[G]; A3: for k being non empty Nat st S1[k] holds S1[k + 1] by A2; let G be finite _Graph; ::_thesis: P1[G] A4: G .order() = G .order() ; A5: S1[1] by A1; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A5, A3); hence P1[G] by A4; ::_thesis: verum end; scheme :: GLIB_000:sch 2 FinGraphSizeInd{ P1[ finite _Graph] } : for G being finite _Graph holds P1[G] provided A1: for G being finite _Graph st G .size() = 0 holds P1[G] and A2: for k being Element of NAT st ( for Gk being finite _Graph st Gk .size() = k holds P1[Gk] ) holds for Gk1 being finite _Graph st Gk1 .size() = k + 1 holds P1[Gk1] proof defpred S1[ Element of NAT ] means for G being finite _Graph st G .size() = $1 holds P1[G]; A3: for k being Element of NAT st S1[k] holds S1[k + 1] by A2; let G be finite _Graph; ::_thesis: P1[G] A4: G .size() = G .size() ; A5: S1[ 0 ] by A1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A3); hence P1[G] by A4; ::_thesis: verum end; definition let G be _Graph; mode Subgraph of G -> _Graph means :Def32: :: GLIB_000:def 32 ( the_Vertices_of it c= the_Vertices_of G & the_Edges_of it c= the_Edges_of G & ( for e being set st e in the_Edges_of it holds ( (the_Source_of it) . e = (the_Source_of G) . e & (the_Target_of it) . e = (the_Target_of G) . e ) ) ); existence ex b1 being _Graph st ( the_Vertices_of b1 c= the_Vertices_of G & the_Edges_of b1 c= the_Edges_of G & ( for e being set st e in the_Edges_of b1 holds ( (the_Source_of b1) . e = (the_Source_of G) . e & (the_Target_of b1) . e = (the_Target_of G) . e ) ) ) proof take G ; ::_thesis: ( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G c= the_Edges_of G & ( for e being set st e in the_Edges_of G holds ( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ) ) thus ( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G c= the_Edges_of G & ( for e being set st e in the_Edges_of G holds ( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def32 defines Subgraph GLIB_000:def_32_:_ for G, b2 being _Graph holds ( b2 is Subgraph of G iff ( the_Vertices_of b2 c= the_Vertices_of G & the_Edges_of b2 c= the_Edges_of G & ( for e being set st e in the_Edges_of b2 holds ( (the_Source_of b2) . e = (the_Source_of G) . e & (the_Target_of b2) . e = (the_Target_of G) . e ) ) ) ); definition let G1 be _Graph; let G2 be Subgraph of G1; :: original: the_Vertices_of redefine func the_Vertices_of G2 -> non empty Subset of (the_Vertices_of G1); coherence the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by Def32; :: original: the_Edges_of redefine func the_Edges_of G2 -> Subset of (the_Edges_of G1); coherence the_Edges_of G2 is Subset of (the_Edges_of G1) by Def32; end; registration let G be _Graph; cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple for Subgraph of G; existence ex b1 being Subgraph of G st ( b1 is trivial & b1 is simple ) proof set v = the Element of the_Vertices_of G; set V = { the Element of the_Vertices_of G}; set E = {} ; reconsider S = {} as Function of {},{ the Element of the_Vertices_of G} by RELSET_1:12; set IT = createGraph ({ the Element of the_Vertices_of G},{},S,S); A1: ( the_Vertices_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) = { the Element of the_Vertices_of G} & ( for e being set st e in the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) holds ( (the_Source_of (createGraph ({ the Element of the_Vertices_of G},{},S,S))) . e = (the_Source_of G) . e & (the_Target_of (createGraph ({ the Element of the_Vertices_of G},{},S,S))) . e = (the_Target_of G) . e ) ) ) by FINSEQ_4:76; the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) = {} by FINSEQ_4:76; then the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) c= the_Edges_of G by XBOOLE_1:2; then reconsider IT = createGraph ({ the Element of the_Vertices_of G},{},S,S) as Subgraph of G by A1, Def32; take IT ; ::_thesis: ( IT is trivial & IT is simple ) thus ( IT is trivial & IT is simple ) ; ::_thesis: verum end; end; Lm4: for G being _Graph holds G is Subgraph of G proof let G be _Graph; ::_thesis: G is Subgraph of G for e being set st e in the_Edges_of G holds ( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ; hence G is Subgraph of G by Def32; ::_thesis: verum end; Lm5: for G1 being _Graph for G2 being Subgraph of G1 for x, y, e being set st e Joins x,y,G2 holds e Joins x,y,G1 proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for x, y, e being set st e Joins x,y,G2 holds e Joins x,y,G1 let G2 be Subgraph of G1; ::_thesis: for x, y, e being set st e Joins x,y,G2 holds e Joins x,y,G1 let x, y, e be set ; ::_thesis: ( e Joins x,y,G2 implies e Joins x,y,G1 ) assume A1: e Joins x,y,G2 ; ::_thesis: e Joins x,y,G1 then A2: e in the_Edges_of G2 by Def13; ( ( (the_Source_of G2) . e = x & (the_Target_of G2) . e = y ) or ( (the_Source_of G2) . e = y & (the_Target_of G2) . e = x ) ) by A1, Def13; then ( ( (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) or ( (the_Source_of G1) . e = y & (the_Target_of G1) . e = x ) ) by A2, Def32; hence e Joins x,y,G1 by A2, Def13; ::_thesis: verum end; registration let G be finite _Graph; cluster -> finite for Subgraph of G; coherence for b1 being Subgraph of G holds b1 is finite proof let G2 be Subgraph of G; ::_thesis: G2 is finite ( the_Vertices_of G2 is finite & the_Edges_of G2 is finite ) ; hence G2 is finite by Def17; ::_thesis: verum end; end; registration let G be loopless _Graph; cluster -> loopless for Subgraph of G; coherence for b1 being Subgraph of G holds b1 is loopless proof let G2 be Subgraph of G; ::_thesis: G2 is loopless now__::_thesis:_for_e_being_set_holds_ (_not_e_in_the_Edges_of_G2_or_not_(the_Source_of_G2)_._e_=_(the_Target_of_G2)_._e_) given e being set such that A1: e in the_Edges_of G2 and A2: (the_Source_of G2) . e = (the_Target_of G2) . e ; ::_thesis: contradiction ( (the_Source_of G2) . e = (the_Source_of G) . e & (the_Target_of G2) . e = (the_Target_of G) . e ) by A1, Def32; hence contradiction by A1, A2, Def18; ::_thesis: verum end; hence G2 is loopless by Def18; ::_thesis: verum end; end; registration let G be trivial _Graph; cluster -> trivial for Subgraph of G; coherence for b1 being Subgraph of G holds b1 is trivial proof let G2 be Subgraph of G; ::_thesis: G2 is trivial card (the_Vertices_of G) = 1 by Def19; then consider v being set such that A1: the_Vertices_of G = {v} by CARD_2:42; the_Vertices_of G2 = {v} by A1, ZFMISC_1:33; then card (the_Vertices_of G2) = 1 by CARD_1:30; hence G2 is trivial by Def19; ::_thesis: verum end; end; registration let G be non-multi _Graph; cluster -> non-multi for Subgraph of G; coherence for b1 being Subgraph of G holds b1 is non-multi proof let G2 be Subgraph of G; ::_thesis: G2 is non-multi now__::_thesis:_for_e1,_e2,_v1,_v2_being_set_st_e1_Joins_v1,v2,G2_&_e2_Joins_v1,v2,G2_holds_ e1_=_e2 let e1, e2, v1, v2 be set ; ::_thesis: ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 implies e1 = e2 ) assume ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 ) ; ::_thesis: e1 = e2 then ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by Lm5; hence e1 = e2 by Def20; ::_thesis: verum end; hence G2 is non-multi by Def20; ::_thesis: verum end; end; definition let G1 be _Graph; let G2 be Subgraph of G1; attrG2 is spanning means :Def33: :: GLIB_000:def 33 the_Vertices_of G2 = the_Vertices_of G1; end; :: deftheorem Def33 defines spanning GLIB_000:def_33_:_ for G1 being _Graph for G2 being Subgraph of G1 holds ( G2 is spanning iff the_Vertices_of G2 = the_Vertices_of G1 ); registration let G be _Graph; cluster Relation-like NAT -defined Function-like finite [Graph-like] spanning for Subgraph of G; existence ex b1 being Subgraph of G st b1 is spanning proof reconsider G9 = G as Subgraph of G by Lm4; take G9 ; ::_thesis: G9 is spanning the_Vertices_of G9 = the_Vertices_of G ; hence G9 is spanning by Def33; ::_thesis: verum end; end; definition let G1, G2 be _Graph; predG1 == G2 means :Def34: :: GLIB_000:def 34 ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ); reflexivity for G1 being _Graph holds ( the_Vertices_of G1 = the_Vertices_of G1 & the_Edges_of G1 = the_Edges_of G1 & the_Source_of G1 = the_Source_of G1 & the_Target_of G1 = the_Target_of G1 ) ; symmetry for G1, G2 being _Graph st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 = the_Source_of G1 & the_Target_of G2 = the_Target_of G1 ) ; end; :: deftheorem Def34 defines == GLIB_000:def_34_:_ for G1, G2 being _Graph holds ( G1 == G2 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ); notation let G1, G2 be _Graph; antonym G1 != G2 for G1 == G2; end; definition let G1, G2 be _Graph; predG1 c= G2 means :Def35: :: GLIB_000:def 35 G1 is Subgraph of G2; reflexivity for G1 being _Graph holds G1 is Subgraph of G1 by Lm4; end; :: deftheorem Def35 defines c= GLIB_000:def_35_:_ for G1, G2 being _Graph holds ( G1 c= G2 iff G1 is Subgraph of G2 ); definition let G1, G2 be _Graph; predG1 c< G2 means :Def36: :: GLIB_000:def 36 ( G1 c= G2 & G1 != G2 ); irreflexivity for G1 being _Graph holds ( not G1 c= G1 or not G1 != G1 ) ; end; :: deftheorem Def36 defines c< GLIB_000:def_36_:_ for G1, G2 being _Graph holds ( G1 c< G2 iff ( G1 c= G2 & G1 != G2 ) ); definition let G be _Graph; let V, E be set ; mode inducedSubgraph of G,V,E -> Subgraph of G means :Def37: :: GLIB_000:def 37 ( the_Vertices_of it = V & the_Edges_of it = E ) if ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) otherwise it == G; existence ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ex b1 being Subgraph of G st ( the_Vertices_of b1 = V & the_Edges_of b1 = E ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b1 being Subgraph of G st b1 == G ) ) proof hereby ::_thesis: ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b1 being Subgraph of G st b1 == G ) assume that A1: V is non empty Subset of (the_Vertices_of G) and A2: E c= G .edgesBetween V ; ::_thesis: ex IT being Subgraph of G st ( the_Vertices_of IT = V & the_Edges_of IT = E ) reconsider E9 = E as Subset of (the_Edges_of G) by A2, XBOOLE_1:1; set S = (the_Source_of G) | E9; set T = (the_Target_of G) | E9; reconsider V9 = V as non empty Subset of (the_Vertices_of G) by A1; dom (the_Target_of G) = the_Edges_of G by FUNCT_2:def_1; then A3: dom ((the_Target_of G) | E9) = E9 by RELAT_1:62; now__::_thesis:_for_e_being_set_st_e_in_E9_holds_ ((the_Target_of_G)_|_E9)_._e_in_V let e be set ; ::_thesis: ( e in E9 implies ((the_Target_of G) | E9) . e in V ) assume A4: e in E9 ; ::_thesis: ((the_Target_of G) | E9) . e in V then e in G .edgesInto V by A2, XBOOLE_0:def_4; then (the_Target_of G) . e in V by Def26; hence ((the_Target_of G) | E9) . e in V by A4, FUNCT_1:49; ::_thesis: verum end; then reconsider T = (the_Target_of G) | E9 as Function of E9,V9 by A3, FUNCT_2:3; dom (the_Source_of G) = the_Edges_of G by FUNCT_2:def_1; then A5: dom ((the_Source_of G) | E9) = E9 by RELAT_1:62; now__::_thesis:_for_e_being_set_st_e_in_E9_holds_ ((the_Source_of_G)_|_E9)_._e_in_V let e be set ; ::_thesis: ( e in E9 implies ((the_Source_of G) | E9) . e in V ) assume A6: e in E9 ; ::_thesis: ((the_Source_of G) | E9) . e in V then e in G .edgesOutOf V by A2, XBOOLE_0:def_4; then (the_Source_of G) . e in V by Def27; hence ((the_Source_of G) | E9) . e in V by A6, FUNCT_1:49; ::_thesis: verum end; then reconsider S = (the_Source_of G) | E9 as Function of E9,V9 by A5, FUNCT_2:3; set IT = createGraph (V9,E9,S,T); A7: the_Edges_of (createGraph (V9,E9,S,T)) = E by FINSEQ_4:76; ( the_Source_of (createGraph (V9,E9,S,T)) = S & the_Target_of (createGraph (V9,E9,S,T)) = T ) by FINSEQ_4:76; then ( the_Vertices_of (createGraph (V9,E9,S,T)) = V & ( for e being set st e in the_Edges_of (createGraph (V9,E9,S,T)) holds ( (the_Source_of (createGraph (V9,E9,S,T))) . e = (the_Source_of G) . e & (the_Target_of (createGraph (V9,E9,S,T))) . e = (the_Target_of G) . e ) ) ) by A7, FINSEQ_4:76, FUNCT_1:49; then reconsider IT = createGraph (V9,E9,S,T) as Subgraph of G by A7, Def32; take IT = IT; ::_thesis: ( the_Vertices_of IT = V & the_Edges_of IT = E ) thus ( the_Vertices_of IT = V & the_Edges_of IT = E ) by FINSEQ_4:76; ::_thesis: verum end; G is Subgraph of G by Lm4; hence ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b1 being Subgraph of G st b1 == G ) ; ::_thesis: verum end; consistency for b1 being Subgraph of G holds verum ; end; :: deftheorem Def37 defines inducedSubgraph GLIB_000:def_37_:_ for G being _Graph for V, E being set for b4 being Subgraph of G holds ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b4 is inducedSubgraph of G,V,E iff ( the_Vertices_of b4 = V & the_Edges_of b4 = E ) ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b4 is inducedSubgraph of G,V,E iff b4 == G ) ) ); definition let G be _Graph; let V be set ; mode inducedSubgraph of G,V is inducedSubgraph of G,V,G .edgesBetween V; end; registration let G be _Graph; let V be non empty finite Subset of (the_Vertices_of G); let E be finite Subset of (G .edgesBetween V); cluster -> finite for inducedSubgraph of G,V,E; coherence for b1 being inducedSubgraph of G,V,E holds b1 is finite proof let IT be inducedSubgraph of G,V,E; ::_thesis: IT is finite ( the_Vertices_of IT = V & the_Edges_of IT = E ) by Def37; hence IT is finite by Def17; ::_thesis: verum end; end; registration let G be _Graph; let v be Element of the_Vertices_of G; let E be Subset of (G .edgesBetween {v}); cluster -> trivial for inducedSubgraph of G,{v},E; coherence for b1 being inducedSubgraph of G,{v},E holds b1 is trivial proof let IT be inducedSubgraph of G,{v},E; ::_thesis: IT is trivial the_Vertices_of IT = {v} by Def37; then card (the_Vertices_of IT) = 1 by CARD_1:30; hence IT is trivial by Def19; ::_thesis: verum end; end; registration let G be _Graph; let v be Element of the_Vertices_of G; cluster -> finite trivial for inducedSubgraph of G,{v}, {} ; coherence for b1 being inducedSubgraph of G,{v}, {} holds ( b1 is finite & b1 is trivial ) proof reconsider E = {} as finite Subset of (G .edgesBetween {v}) by XBOOLE_1:2; let IT be inducedSubgraph of G,{v}, {} ; ::_thesis: ( IT is finite & IT is trivial ) IT is inducedSubgraph of G,{v},E ; hence ( IT is finite & IT is trivial ) ; ::_thesis: verum end; end; registration let G be _Graph; let V be non empty Subset of (the_Vertices_of G); cluster -> simple for inducedSubgraph of G,V, {} ; coherence for b1 being inducedSubgraph of G,V, {} holds b1 is simple proof let IT be inducedSubgraph of G,V, {} ; ::_thesis: IT is simple reconsider E = {} as Subset of (G .edgesBetween V) by XBOOLE_1:2; IT is inducedSubgraph of G,V,E ; then the_Edges_of IT = {} by Def37; hence IT is simple by Lm3; ::_thesis: verum end; end; Lm6: for G being _Graph for e, X being set holds ( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X ) proof let G be _Graph; ::_thesis: for e, X being set holds ( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X ) let e, X be set ; ::_thesis: ( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X ) hereby ::_thesis: ( e in G .edgesBetween X implies ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) ) assume ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) ; ::_thesis: e in G .edgesBetween X then ( e in G .edgesInto X & e in G .edgesOutOf X ) by Def26, Def27; hence e in G .edgesBetween X by XBOOLE_0:def_4; ::_thesis: verum end; assume e in G .edgesBetween X ; ::_thesis: ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) then ( e in G .edgesInto X & e in G .edgesOutOf X ) by XBOOLE_0:def_4; hence ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) by Def26, Def27; ::_thesis: verum end; Lm7: for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G) proof let G be _Graph; ::_thesis: the_Edges_of G = G .edgesBetween (the_Vertices_of G) set EG = the_Edges_of G; set SG = the_Source_of G; set TG = the_Target_of G; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_Edges_of_G_implies_x_in_G_.edgesBetween_(the_Vertices_of_G)_)_&_(_x_in_G_.edgesBetween_(the_Vertices_of_G)_implies_x_in_the_Edges_of_G_)_) let x be set ; ::_thesis: ( ( x in the_Edges_of G implies x in G .edgesBetween (the_Vertices_of G) ) & ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G ) ) hereby ::_thesis: ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G ) assume A1: x in the_Edges_of G ; ::_thesis: x in G .edgesBetween (the_Vertices_of G) then ( (the_Source_of G) . x in the_Vertices_of G & (the_Target_of G) . x in the_Vertices_of G ) by FUNCT_2:5; hence x in G .edgesBetween (the_Vertices_of G) by A1, Lm6; ::_thesis: verum end; assume x in G .edgesBetween (the_Vertices_of G) ; ::_thesis: x in the_Edges_of G hence x in the_Edges_of G ; ::_thesis: verum end; hence the_Edges_of G = G .edgesBetween (the_Vertices_of G) by TARSKI:1; ::_thesis: verum end; registration let G be _Graph; let E be Subset of (the_Edges_of G); cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,E; coherence for b1 being inducedSubgraph of G, the_Vertices_of G,E holds b1 is spanning proof let G1 be inducedSubgraph of G, the_Vertices_of G,E; ::_thesis: G1 is spanning ( G .edgesBetween (the_Vertices_of G) = the_Edges_of G & the_Vertices_of G c= the_Vertices_of G ) by Lm7; then the_Vertices_of G1 = the_Vertices_of G by Def37; hence G1 is spanning by Def33; ::_thesis: verum end; end; registration let G be _Graph; cluster -> spanning for inducedSubgraph of G, the_Vertices_of G, {} ; coherence for b1 being inducedSubgraph of G, the_Vertices_of G, {} holds b1 is spanning proof let G1 be inducedSubgraph of G, the_Vertices_of G, {} ; ::_thesis: G1 is spanning ( the_Vertices_of G c= the_Vertices_of G & {} c= G .edgesBetween (the_Vertices_of G) ) by XBOOLE_1:2; then the_Vertices_of G1 = the_Vertices_of G by Def37; hence G1 is spanning by Def33; ::_thesis: verum end; end; definition let G be _Graph; let v be set ; mode removeVertex of G,v is inducedSubgraph of G,((the_Vertices_of G) \ {v}); end; definition let G be _Graph; let V be set ; mode removeVertices of G,V is inducedSubgraph of G,((the_Vertices_of G) \ V); end; definition let G be _Graph; let e be set ; mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e}; end; definition let G be _Graph; let E be set ; mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E; end; registration let G be _Graph; let e be set ; cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e}; coherence for b1 being removeEdge of G,e holds b1 is spanning ; end; registration let G be _Graph; let E be set ; cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E; coherence for b1 being removeEdges of G,E holds b1 is spanning ; end; definition let G be _Graph; mode Vertex of G is Element of the_Vertices_of G; end; definition let G be _Graph; let v be Vertex of G; funcv .edgesIn() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 38 G .edgesInto {v}; coherence G .edgesInto {v} is Subset of (the_Edges_of G) ; funcv .edgesOut() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 39 G .edgesOutOf {v}; coherence G .edgesOutOf {v} is Subset of (the_Edges_of G) ; funcv .edgesInOut() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 40 G .edgesInOut {v}; coherence G .edgesInOut {v} is Subset of (the_Edges_of G) ; end; :: deftheorem defines .edgesIn() GLIB_000:def_38_:_ for G being _Graph for v being Vertex of G holds v .edgesIn() = G .edgesInto {v}; :: deftheorem defines .edgesOut() GLIB_000:def_39_:_ for G being _Graph for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v}; :: deftheorem defines .edgesInOut() GLIB_000:def_40_:_ for G being _Graph for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v}; Lm8: for G being _Graph for v being Vertex of G for e being set holds ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) proof let G be _Graph; ::_thesis: for v being Vertex of G for e being set holds ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) let v be Vertex of G; ::_thesis: for e being set holds ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) let e be set ; ::_thesis: ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) hereby ::_thesis: ( e in the_Edges_of G & (the_Target_of G) . e = v implies e in v .edgesIn() ) assume A1: e in v .edgesIn() ; ::_thesis: ( e in the_Edges_of G & (the_Target_of G) . e = v ) then (the_Target_of G) . e in {v} by Def26; hence ( e in the_Edges_of G & (the_Target_of G) . e = v ) by A1, TARSKI:def_1; ::_thesis: verum end; assume that A2: e in the_Edges_of G and A3: (the_Target_of G) . e = v ; ::_thesis: e in v .edgesIn() (the_Target_of G) . e in {v} by A3, TARSKI:def_1; hence e in v .edgesIn() by A2, Def26; ::_thesis: verum end; Lm9: for G being _Graph for v being Vertex of G for e being set holds ( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) proof let G be _Graph; ::_thesis: for v being Vertex of G for e being set holds ( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) let v be Vertex of G; ::_thesis: for e being set holds ( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) let e be set ; ::_thesis: ( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) hereby ::_thesis: ( e in the_Edges_of G & (the_Source_of G) . e = v implies e in v .edgesOut() ) assume A1: e in v .edgesOut() ; ::_thesis: ( e in the_Edges_of G & (the_Source_of G) . e = v ) then (the_Source_of G) . e in {v} by Def27; hence ( e in the_Edges_of G & (the_Source_of G) . e = v ) by A1, TARSKI:def_1; ::_thesis: verum end; assume that A2: e in the_Edges_of G and A3: (the_Source_of G) . e = v ; ::_thesis: e in v .edgesOut() (the_Source_of G) . e in {v} by A3, TARSKI:def_1; hence e in v .edgesOut() by A2, Def27; ::_thesis: verum end; definition let G be _Graph; let v be Vertex of G; let e be set ; funcv .adj e -> Vertex of G equals :Def41: :: GLIB_000:def 41 (the_Source_of G) . e if ( e in the_Edges_of G & (the_Target_of G) . e = v ) (the_Target_of G) . e if ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v ) otherwise v; coherence ( ( e in the_Edges_of G & (the_Target_of G) . e = v implies (the_Source_of G) . e is Vertex of G ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies (the_Target_of G) . e is Vertex of G ) & ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) & ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v is Vertex of G ) ) by FUNCT_2:5; consistency for b1 being Vertex of G st e in the_Edges_of G & (the_Target_of G) . e = v & e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v holds ( b1 = (the_Source_of G) . e iff b1 = (the_Target_of G) . e ) ; end; :: deftheorem Def41 defines .adj GLIB_000:def_41_:_ for G being _Graph for v being Vertex of G for e being set holds ( ( e in the_Edges_of G & (the_Target_of G) . e = v implies v .adj e = (the_Source_of G) . e ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies v .adj e = (the_Target_of G) . e ) & ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) & ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v .adj e = v ) ); definition let G be _Graph; let v be Vertex of G; funcv .inDegree() -> Cardinal equals :: GLIB_000:def 42 card (v .edgesIn()); coherence card (v .edgesIn()) is Cardinal ; funcv .outDegree() -> Cardinal equals :: GLIB_000:def 43 card (v .edgesOut()); coherence card (v .edgesOut()) is Cardinal ; end; :: deftheorem defines .inDegree() GLIB_000:def_42_:_ for G being _Graph for v being Vertex of G holds v .inDegree() = card (v .edgesIn()); :: deftheorem defines .outDegree() GLIB_000:def_43_:_ for G being _Graph for v being Vertex of G holds v .outDegree() = card (v .edgesOut()); definition let G be finite _Graph; let v be Vertex of G; :: original: .inDegree() redefine funcv .inDegree() -> Element of NAT ; coherence v .inDegree() is Element of NAT proof v .inDegree() = card (v .edgesIn()) ; hence v .inDegree() is Element of NAT ; ::_thesis: verum end; :: original: .outDegree() redefine funcv .outDegree() -> Element of NAT ; coherence v .outDegree() is Element of NAT proof v .outDegree() = card (v .edgesOut()) ; hence v .outDegree() is Element of NAT ; ::_thesis: verum end; end; definition let G be _Graph; let v be Vertex of G; funcv .degree() -> Cardinal equals :: GLIB_000:def 44 (v .inDegree()) +` (v .outDegree()); coherence (v .inDegree()) +` (v .outDegree()) is Cardinal ; end; :: deftheorem defines .degree() GLIB_000:def_44_:_ for G being _Graph for v being Vertex of G holds v .degree() = (v .inDegree()) +` (v .outDegree()); definition let G be finite _Graph; let v be Vertex of G; :: original: .degree() redefine funcv .degree() -> Element of NAT equals :: GLIB_000:def 45 (v .inDegree()) + (v .outDegree()); correctness coherence v .degree() is Element of NAT ; compatibility for b1 being Element of NAT holds ( b1 = v .degree() iff b1 = (v .inDegree()) + (v .outDegree()) ); proof v .degree() = card ((v .inDegree()) +^ (v .outDegree())) by CARD_2:def_1 .= card ((v .inDegree()) + (v .outDegree())) by CARD_2:36 .= (v .inDegree()) + (v .outDegree()) by CARD_1:def_2 ; hence ( v .degree() is Element of NAT & ( for b1 being Element of NAT holds ( b1 = v .degree() iff b1 = (v .inDegree()) + (v .outDegree()) ) ) ) ; ::_thesis: verum end; end; :: deftheorem defines .degree() GLIB_000:def_45_:_ for G being finite _Graph for v being Vertex of G holds v .degree() = (v .inDegree()) + (v .outDegree()); definition let G be _Graph; let v be Vertex of G; funcv .inNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 46 (the_Source_of G) .: (v .edgesIn()); coherence (the_Source_of G) .: (v .edgesIn()) is Subset of (the_Vertices_of G) ; funcv .outNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 47 (the_Target_of G) .: (v .edgesOut()); coherence (the_Target_of G) .: (v .edgesOut()) is Subset of (the_Vertices_of G) ; end; :: deftheorem defines .inNeighbors() GLIB_000:def_46_:_ for G being _Graph for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn()); :: deftheorem defines .outNeighbors() GLIB_000:def_47_:_ for G being _Graph for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut()); definition let G be _Graph; let v be Vertex of G; funcv .allNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 48 (v .inNeighbors()) \/ (v .outNeighbors()); coherence (v .inNeighbors()) \/ (v .outNeighbors()) is Subset of (the_Vertices_of G) ; end; :: deftheorem defines .allNeighbors() GLIB_000:def_48_:_ for G being _Graph for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors()); definition let G be _Graph; let v be Vertex of G; attrv is isolated means :Def49: :: GLIB_000:def 49 v .edgesInOut() = {} ; end; :: deftheorem Def49 defines isolated GLIB_000:def_49_:_ for G being _Graph for v being Vertex of G holds ( v is isolated iff v .edgesInOut() = {} ); definition let G be finite _Graph; let v be Vertex of G; redefine attr v is isolated means :: GLIB_000:def 50 v .degree() = 0 ; compatibility ( v is isolated iff v .degree() = 0 ) proof hereby ::_thesis: ( v .degree() = 0 implies v is isolated ) assume v is isolated ; ::_thesis: v .degree() = 0 then A1: v .edgesInOut() = {} by Def49; then v .inDegree() = 0 by CARD_1:27, XBOOLE_1:15; hence v .degree() = 0 by A1, CARD_1:27, XBOOLE_1:15; ::_thesis: verum end; assume A2: v .degree() = 0 ; ::_thesis: v is isolated then v .edgesIn() = {} ; then v .edgesInOut() = {} by A2; hence v is isolated by Def49; ::_thesis: verum end; end; :: deftheorem defines isolated GLIB_000:def_50_:_ for G being finite _Graph for v being Vertex of G holds ( v is isolated iff v .degree() = 0 ); definition let G be _Graph; let v be Vertex of G; attrv is endvertex means :Def51: :: GLIB_000:def 51 ex e being set st ( v .edgesInOut() = {e} & not e Joins v,v,G ); end; :: deftheorem Def51 defines endvertex GLIB_000:def_51_:_ for G being _Graph for v being Vertex of G holds ( v is endvertex iff ex e being set st ( v .edgesInOut() = {e} & not e Joins v,v,G ) ); definition let G be finite _Graph; let v be Vertex of G; redefine attr v is endvertex means :: GLIB_000:def 52 v .degree() = 1; compatibility ( v is endvertex iff v .degree() = 1 ) proof hereby ::_thesis: ( v .degree() = 1 implies v is endvertex ) assume v is endvertex ; ::_thesis: v .degree() = 1 then consider e being set such that A1: v .edgesInOut() = {e} and A2: not e Joins v,v,G by Def51; now__::_thesis:_v_.degree()_=_1 percases ( ( v .edgesIn() = {e} & v .edgesOut() = {e} ) or ( v .edgesIn() = {} & v .edgesOut() = {e} ) or ( v .edgesIn() = {e} & v .edgesOut() = {} ) ) by A1, ZFMISC_1:37; supposeA3: ( v .edgesIn() = {e} & v .edgesOut() = {e} ) ; ::_thesis: v .degree() = 1 then e in v .edgesOut() by TARSKI:def_1; then A4: (the_Source_of G) . e = v by Lm9; A5: e in v .edgesIn() by A3, TARSKI:def_1; then (the_Target_of G) . e = v by Lm8; hence v .degree() = 1 by A2, A5, A4, Def13; ::_thesis: verum end; suppose ( v .edgesIn() = {} & v .edgesOut() = {e} ) ; ::_thesis: v .degree() = 1 hence v .degree() = 1 by CARD_1:27, CARD_1:30; ::_thesis: verum end; suppose ( v .edgesIn() = {e} & v .edgesOut() = {} ) ; ::_thesis: v .degree() = 1 hence v .degree() = 1 by CARD_1:27, CARD_1:30; ::_thesis: verum end; end; end; hence v .degree() = 1 ; ::_thesis: verum end; assume A6: v .degree() = 1 ; ::_thesis: v is endvertex now__::_thesis:_v_is_endvertex percases ( card (v .edgesIn()) = 0 or card (v .edgesIn()) <> 0 ) ; supposeA7: card (v .edgesIn()) = 0 ; ::_thesis: v is endvertex then consider e being set such that A8: v .edgesOut() = {e} by A6, CARD_2:42; A9: v .edgesIn() = {} by A7; A10: now__::_thesis:_not_e_Joins_v,v,G assume e Joins v,v,G ; ::_thesis: contradiction then ( e in the_Edges_of G & (the_Target_of G) . e = v ) by Def13; hence contradiction by A9, Lm8; ::_thesis: verum end; v .edgesInOut() = {e} by A9, A8; hence v is endvertex by A10, Def51; ::_thesis: verum end; suppose card (v .edgesIn()) <> 0 ; ::_thesis: v is endvertex then 0 < card (v .edgesIn()) by NAT_1:3; then A11: 0 + 1 <= card (v .edgesIn()) by NAT_1:13; card (v .edgesIn()) <= 1 by A6, NAT_1:11; then A12: card (v .edgesIn()) = 1 by A11, XXREAL_0:1; then consider e being set such that A13: v .edgesIn() = {e} by CARD_2:42; A14: v .edgesOut() = {} by A6, A12; A15: now__::_thesis:_not_e_Joins_v,v,G assume e Joins v,v,G ; ::_thesis: contradiction then ( e in the_Edges_of G & (the_Source_of G) . e = v ) by Def13; hence contradiction by A14, Lm9; ::_thesis: verum end; v .edgesInOut() = {e} by A13, A14; hence v is endvertex by A15, Def51; ::_thesis: verum end; end; end; hence v is endvertex ; ::_thesis: verum end; end; :: deftheorem defines endvertex GLIB_000:def_52_:_ for G being finite _Graph for v being Vertex of G holds ( v is endvertex iff v .degree() = 1 ); definition let F be ManySortedSet of NAT ; attrF is Graph-yielding means :Def53: :: GLIB_000:def 53 for n being Nat holds F . n is _Graph; attrF is halting means :Def54: :: GLIB_000:def 54 ex n being Nat st F . n = F . (n + 1); end; :: deftheorem Def53 defines Graph-yielding GLIB_000:def_53_:_ for F being ManySortedSet of NAT holds ( F is Graph-yielding iff for n being Nat holds F . n is _Graph ); :: deftheorem Def54 defines halting GLIB_000:def_54_:_ for F being ManySortedSet of NAT holds ( F is halting iff ex n being Nat st F . n = F . (n + 1) ); definition let F be ManySortedSet of NAT ; funcF .Lifespan() -> Element of NAT means :: GLIB_000:def 55 ( F . it = F . (it + 1) & ( for n being Nat st F . n = F . (n + 1) holds it <= n ) ) if F is halting otherwise it = 0 ; existence ( ( F is halting implies ex b1 being Element of NAT st ( F . b1 = F . (b1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds b1 <= n ) ) ) & ( not F is halting implies ex b1 being Element of NAT st b1 = 0 ) ) proof defpred S1[ Nat] means F . $1 = F . ($1 + 1); hereby ::_thesis: ( not F is halting implies ex b1 being Element of NAT st b1 = 0 ) assume F is halting ; ::_thesis: ex IT being Element of NAT st ( S1[IT] & ( for n being Nat st S1[n] holds IT <= n ) ) then A1: ex n being Nat st S1[n] by Def54; ex IT being Nat st ( S1[IT] & ( for n being Nat st S1[n] holds IT <= n ) ) from NAT_1:sch_5(A1); then consider IT being Nat such that A2: ( S1[IT] & ( for n being Nat st S1[n] holds IT <= n ) ) ; IT in NAT by ORDINAL1:def_12; hence ex IT being Element of NAT st ( S1[IT] & ( for n being Nat st S1[n] holds IT <= n ) ) by A2; ::_thesis: verum end; thus ( not F is halting implies ex b1 being Element of NAT st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT holds ( ( F is halting & F . b1 = F . (b1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds b1 <= n ) & F . b2 = F . (b2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds b2 <= n ) implies b1 = b2 ) & ( not F is halting & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let IT1, IT2 be Element of NAT ; ::_thesis: ( ( F is halting & F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT1 <= n ) & F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT2 <= n ) implies IT1 = IT2 ) & ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ) hereby ::_thesis: ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) assume F is halting ; ::_thesis: ( F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT1 <= n ) & F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT2 <= n ) implies IT1 = IT2 ) assume A3: ( F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT1 <= n ) ) ; ::_thesis: ( F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT2 <= n ) implies IT1 = IT2 ) assume ( F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds IT2 <= n ) ) ; ::_thesis: IT1 = IT2 then ( IT1 <= IT2 & IT2 <= IT1 ) by A3; hence IT1 = IT2 by XXREAL_0:1; ::_thesis: verum end; thus ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; ::_thesis: verum end; consistency for b1 being Element of NAT holds verum ; end; :: deftheorem defines .Lifespan() GLIB_000:def_55_:_ for F being ManySortedSet of NAT for b2 being Element of NAT holds ( ( F is halting implies ( b2 = F .Lifespan() iff ( F . b2 = F . (b2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds b2 <= n ) ) ) ) & ( not F is halting implies ( b2 = F .Lifespan() iff b2 = 0 ) ) ); definition let F be ManySortedSet of NAT ; funcF .Result() -> set equals :: GLIB_000:def 56 F . (F .Lifespan()); coherence F . (F .Lifespan()) is set ; end; :: deftheorem defines .Result() GLIB_000:def_56_:_ for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan()); registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding for set ; existence ex b1 being ManySortedSet of NAT st b1 is Graph-yielding proof set G = the _Graph; set F = NAT --> the _Graph; A1: dom (NAT --> the _Graph) = NAT by FUNCOP_1:13; reconsider F = NAT --> the _Graph as ManySortedSet of NAT ; take F ; ::_thesis: F is Graph-yielding let x be Nat; :: according to GLIB_000:def_53 ::_thesis: F . x is _Graph x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the _Graph} by FUNCOP_1:8; hence F . x is _Graph by TARSKI:def_1; ::_thesis: verum end; end; definition mode GraphSeq is Graph-yielding ManySortedSet of NAT ; end; registration let GSq be GraphSeq; let x be Nat; clusterGSq . x -> Relation-like Function-like ; coherence ( GSq . x is Function-like & GSq . x is Relation-like ) by Def53; end; registration let GSq be GraphSeq; let x be Nat; clusterGSq . x -> NAT -defined finite ; coherence ( GSq . x is NAT -defined & GSq . x is finite ) by Def53; end; registration let GSq be GraphSeq; let x be Nat; clusterGSq . x -> [Graph-like] ; coherence GSq . x is [Graph-like] by Def53; end; definition let GSq be GraphSeq; attrGSq is finite means :Def57: :: GLIB_000:def 57 for x being Nat holds GSq . x is finite ; attrGSq is loopless means :Def58: :: GLIB_000:def 58 for x being Nat holds GSq . x is loopless ; attrGSq is trivial means :Def59: :: GLIB_000:def 59 for x being Nat holds GSq . x is trivial ; attrGSq is non-trivial means :Def60: :: GLIB_000:def 60 for x being Nat holds not GSq . x is trivial ; attrGSq is non-multi means :Def61: :: GLIB_000:def 61 for x being Nat holds GSq . x is non-multi ; attrGSq is non-Dmulti means :Def62: :: GLIB_000:def 62 for x being Nat holds GSq . x is non-Dmulti ; attrGSq is simple means :Def63: :: GLIB_000:def 63 for x being Nat holds GSq . x is simple ; attrGSq is Dsimple means :Def64: :: GLIB_000:def 64 for x being Nat holds GSq . x is Dsimple ; end; :: deftheorem Def57 defines finite GLIB_000:def_57_:_ for GSq being GraphSeq holds ( GSq is finite iff for x being Nat holds GSq . x is finite ); :: deftheorem Def58 defines loopless GLIB_000:def_58_:_ for GSq being GraphSeq holds ( GSq is loopless iff for x being Nat holds GSq . x is loopless ); :: deftheorem Def59 defines trivial GLIB_000:def_59_:_ for GSq being GraphSeq holds ( GSq is trivial iff for x being Nat holds GSq . x is trivial ); :: deftheorem Def60 defines non-trivial GLIB_000:def_60_:_ for GSq being GraphSeq holds ( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial ); :: deftheorem Def61 defines non-multi GLIB_000:def_61_:_ for GSq being GraphSeq holds ( GSq is non-multi iff for x being Nat holds GSq . x is non-multi ); :: deftheorem Def62 defines non-Dmulti GLIB_000:def_62_:_ for GSq being GraphSeq holds ( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti ); :: deftheorem Def63 defines simple GLIB_000:def_63_:_ for GSq being GraphSeq holds ( GSq is simple iff for x being Nat holds GSq . x is simple ); :: deftheorem Def64 defines Dsimple GLIB_000:def_64_:_ for GSq being GraphSeq holds ( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple ); definition let GSq be GraphSeq; redefine attr GSq is halting means :: GLIB_000:def 65 ex n being Nat st GSq . n = GSq . (n + 1); compatibility ( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) ) by Def54; end; :: deftheorem defines halting GLIB_000:def_65_:_ for GSq being GraphSeq holds ( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) ); registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless trivial non-multi non-Dmulti simple Dsimple for set ; existence ex b1 being GraphSeq st ( b1 is halting & b1 is finite & b1 is loopless & b1 is trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple ) proof set G = the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph; set F = NAT --> the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph; A1: dom (NAT --> the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph) = NAT by FUNCOP_1:13; reconsider F = NAT --> the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph as ManySortedSet of NAT ; now__::_thesis:_for_x_being_Nat_holds_F_._x_is__Graph let x be Nat; ::_thesis: F . x is _Graph x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; hence F . x is _Graph by TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as GraphSeq by Def53; F . (1 + 1) in rng F by A1, FUNCT_1:3; then F . (1 + 1) in { the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; then A2: F . (1 + 1) = the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def_1; take F ; ::_thesis: ( F is halting & F is finite & F is loopless & F is trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) F . 1 in rng F by A1, FUNCT_1:3; then F . 1 in { the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; then F . 1 = the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def_1; hence F is halting by A2, Def54; ::_thesis: ( F is finite & F is loopless & F is trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) now__::_thesis:_for_x_being_Nat_holds_ (_F_._x_is_finite_&_F_._x_is_loopless_&_F_._x_is_trivial_&_F_._x_is_non-multi_&_F_._x_is_non-Dmulti_&_F_._x_is_simple_&_F_._x_is_Dsimple_) let x be Nat; ::_thesis: ( F . x is finite & F . x is loopless & F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple ) x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; hence ( F . x is finite & F . x is loopless & F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple ) by TARSKI:def_1; ::_thesis: verum end; hence ( F is finite & F is loopless & F is trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) by Def57, Def58, Def59, Def61, Def62, Def63, Def64; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless non-trivial non-multi non-Dmulti simple Dsimple for set ; existence ex b1 being GraphSeq st ( b1 is halting & b1 is finite & b1 is loopless & b1 is non-trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple ) proof set G = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph; set F = NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph; A3: dom (NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph) = NAT by FUNCOP_1:13; reconsider F = NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph as ManySortedSet of NAT ; now__::_thesis:_for_x_being_Nat_holds_F_._x_is__Graph let x be Nat; ::_thesis: F . x is _Graph x in NAT by ORDINAL1:def_12; then F . x in rng F by A3, FUNCT_1:3; then F . x in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; hence F . x is _Graph by TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as GraphSeq by Def53; F . (1 + 1) in rng F by A3, FUNCT_1:3; then F . (1 + 1) in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; then A4: F . (1 + 1) = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def_1; take F ; ::_thesis: ( F is halting & F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) F . 1 in rng F by A3, FUNCT_1:3; then F . 1 in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; then F . 1 = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def_1; hence F is halting by A4, Def54; ::_thesis: ( F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) now__::_thesis:_for_x_being_Nat_holds_ (_F_._x_is_finite_&_F_._x_is_loopless_&_not_F_._x_is_trivial_&_F_._x_is_non-multi_&_F_._x_is_non-Dmulti_&_F_._x_is_simple_&_F_._x_is_Dsimple_) let x be Nat; ::_thesis: ( F . x is finite & F . x is loopless & not F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple ) x in NAT by ORDINAL1:def_12; then F . x in rng F by A3, FUNCT_1:3; then F . x in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8; hence ( F . x is finite & F . x is loopless & not F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple ) by TARSKI:def_1; ::_thesis: verum end; hence ( F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) by Def57, Def58, Def60, Def61, Def62, Def63, Def64; ::_thesis: verum end; end; registration let GSq be finite GraphSeq; let x be Nat; clusterGSq . x -> finite ; coherence GSq . x is finite by Def57; end; registration let GSq be loopless GraphSeq; let x be Nat; clusterGSq . x -> loopless for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is loopless by Def58; end; registration let GSq be trivial GraphSeq; let x be Nat; clusterGSq . x -> trivial for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is trivial by Def59; end; registration let GSq be non-trivial GraphSeq; let x be Nat; clusterGSq . x -> non trivial for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds not b1 is trivial by Def60; end; registration let GSq be non-multi GraphSeq; let x be Nat; clusterGSq . x -> non-multi for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is non-multi by Def61; end; registration let GSq be non-Dmulti GraphSeq; let x be Nat; clusterGSq . x -> non-Dmulti for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is non-Dmulti by Def62; end; registration let GSq be simple GraphSeq; let x be Nat; clusterGSq . x -> simple for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is simple by Def63; end; registration let GSq be Dsimple GraphSeq; let x be Nat; clusterGSq . x -> Dsimple for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is Dsimple by Def64; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding non-multi -> non-Dmulti for set ; coherence for b1 being GraphSeq st b1 is non-multi holds b1 is non-Dmulti proof let GS be GraphSeq; ::_thesis: ( GS is non-multi implies GS is non-Dmulti ) assume GS is non-multi ; ::_thesis: GS is non-Dmulti then reconsider GS9 = GS as non-multi GraphSeq ; for x being Nat holds GS9 . x is non-Dmulti ; hence GS is non-Dmulti by Def62; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding simple -> loopless non-multi for set ; coherence for b1 being GraphSeq st b1 is simple holds ( b1 is loopless & b1 is non-multi ) proof let GS be GraphSeq; ::_thesis: ( GS is simple implies ( GS is loopless & GS is non-multi ) ) assume GS is simple ; ::_thesis: ( GS is loopless & GS is non-multi ) then reconsider GS9 = GS as simple GraphSeq ; for x being Nat holds GS9 . x is loopless ; hence GS is loopless by Def58; ::_thesis: GS is non-multi for x being Nat holds GS9 . x is non-multi ; hence GS is non-multi by Def61; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless non-multi -> simple for set ; coherence for b1 being GraphSeq st b1 is loopless & b1 is non-multi holds b1 is simple proof let GS be GraphSeq; ::_thesis: ( GS is loopless & GS is non-multi implies GS is simple ) assume ( GS is loopless & GS is non-multi ) ; ::_thesis: GS is simple then reconsider GS9 = GS as loopless non-multi GraphSeq ; for x being Nat holds GS9 . x is simple ; hence GS is simple by Def63; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless non-Dmulti -> Dsimple for set ; coherence for b1 being GraphSeq st b1 is loopless & b1 is non-Dmulti holds b1 is Dsimple proof let GS be GraphSeq; ::_thesis: ( GS is loopless & GS is non-Dmulti implies GS is Dsimple ) assume ( GS is loopless & GS is non-Dmulti ) ; ::_thesis: GS is Dsimple then reconsider GS9 = GS as loopless non-Dmulti GraphSeq ; for x being Nat holds GS9 . x is Dsimple ; hence GS is Dsimple by Def64; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding Dsimple -> loopless non-Dmulti for set ; coherence for b1 being GraphSeq st b1 is Dsimple holds ( b1 is loopless & b1 is non-Dmulti ) proof let GS be GraphSeq; ::_thesis: ( GS is Dsimple implies ( GS is loopless & GS is non-Dmulti ) ) assume GS is Dsimple ; ::_thesis: ( GS is loopless & GS is non-Dmulti ) then reconsider GS9 = GS as Dsimple GraphSeq ; for x being Nat holds GS9 . x is loopless ; hence GS is loopless by Def58; ::_thesis: GS is non-Dmulti for x being Nat holds GS9 . x is non-Dmulti ; hence GS is non-Dmulti by Def62; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding loopless trivial -> finite for set ; coherence for b1 being GraphSeq st b1 is trivial & b1 is loopless holds b1 is finite proof let GS be GraphSeq; ::_thesis: ( GS is trivial & GS is loopless implies GS is finite ) assume ( GS is trivial & GS is loopless ) ; ::_thesis: GS is finite then reconsider GS9 = GS as loopless trivial GraphSeq ; for x being Nat holds GS9 . x is finite ; hence GS is finite by Def57; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding trivial non-Dmulti -> finite for set ; coherence for b1 being GraphSeq st b1 is trivial & b1 is non-Dmulti holds b1 is finite proof let GS be GraphSeq; ::_thesis: ( GS is trivial & GS is non-Dmulti implies GS is finite ) assume ( GS is trivial & GS is non-Dmulti ) ; ::_thesis: GS is finite then reconsider GS9 = GS as trivial non-Dmulti GraphSeq ; for x being Nat holds GS9 . x is finite ; hence GS is finite by Def57; ::_thesis: verum end; end; begin theorem :: GLIB_000:1 ( VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 & TargetSelector = 4 ) ; theorem :: GLIB_000:2 for G being _Graph holds _GraphSelectors c= dom G proof let G be _Graph; ::_thesis: _GraphSelectors c= dom G now__::_thesis:_for_x_being_set_st_x_in__GraphSelectors_holds_ x_in_dom_G let x be set ; ::_thesis: ( x in _GraphSelectors implies x in dom G ) assume x in _GraphSelectors ; ::_thesis: x in dom G then ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector ) by ENUMSET1:def_2; hence x in dom G by Def10; ::_thesis: verum end; hence _GraphSelectors c= dom G by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:3 for GS being GraphStruct holds ( the_Vertices_of GS = GS . VertexSelector & the_Edges_of GS = GS . EdgeSelector & the_Source_of GS = GS . SourceSelector & the_Target_of GS = GS . TargetSelector ) ; theorem :: GLIB_000:4 for G being _Graph holds ( dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) = the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (the_Target_of G) c= the_Vertices_of G ) by FUNCT_2:def_1; theorem :: GLIB_000:5 for GS being GraphStruct holds ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) by Lm1; theorem :: GLIB_000:6 for V being non empty set for E being set for S, T being Function of E,V holds ( the_Vertices_of (createGraph (V,E,S,T)) = V & the_Edges_of (createGraph (V,E,S,T)) = E & the_Source_of (createGraph (V,E,S,T)) = S & the_Target_of (createGraph (V,E,S,T)) = T ) by FINSEQ_4:76; theorem Th7: :: GLIB_000:7 for GS being GraphStruct for x being set for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n} proof let GS be GraphStruct; ::_thesis: for x being set for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n} let x be set ; ::_thesis: for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n} let n be Nat; ::_thesis: dom (GS .set (n,x)) = (dom GS) \/ {n} set G2 = GS .set (n,x); thus dom (GS .set (n,x)) = (dom GS) \/ (dom (n .--> x)) by FUNCT_4:def_1 .= (dom GS) \/ {n} by FUNCOP_1:13 ; ::_thesis: verum end; theorem Th8: :: GLIB_000:8 for GS being GraphStruct for x being set for n being Nat holds (GS .set (n,x)) . n = x proof let GS be GraphStruct; ::_thesis: for x being set for n being Nat holds (GS .set (n,x)) . n = x let x be set ; ::_thesis: for n being Nat holds (GS .set (n,x)) . n = x let n be Nat; ::_thesis: (GS .set (n,x)) . n = x set G2 = GS .set (n,x); dom (n .--> x) = {n} by FUNCOP_1:13; then n in dom (n .--> x) by TARSKI:def_1; hence (GS .set (n,x)) . n = (n .--> x) . n by FUNCT_4:13 .= x by FUNCOP_1:72 ; ::_thesis: verum end; theorem Th9: :: GLIB_000:9 for GS being GraphStruct for x being set for n1, n2 being Nat st n1 <> n2 holds GS . n2 = (GS .set (n1,x)) . n2 proof let GS be GraphStruct; ::_thesis: for x being set for n1, n2 being Nat st n1 <> n2 holds GS . n2 = (GS .set (n1,x)) . n2 let x be set ; ::_thesis: for n1, n2 being Nat st n1 <> n2 holds GS . n2 = (GS .set (n1,x)) . n2 let n1, n2 be Nat; ::_thesis: ( n1 <> n2 implies GS . n2 = (GS .set (n1,x)) . n2 ) assume n1 <> n2 ; ::_thesis: GS . n2 = (GS .set (n1,x)) . n2 then not n2 in dom (n1 .--> x) by TARSKI:def_1; hence GS . n2 = (GS .set (n1,x)) . n2 by FUNCT_4:11; ::_thesis: verum end; theorem :: GLIB_000:10 for G being _Graph for x being set for n being Nat st not n in _GraphSelectors holds ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) proof let G be _Graph; ::_thesis: for x being set for n being Nat st not n in _GraphSelectors holds ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) let x be set ; ::_thesis: for n being Nat st not n in _GraphSelectors holds ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) let n be Nat; ::_thesis: ( not n in _GraphSelectors implies ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) ) set G2 = G .set (n,x); A1: dom G c= dom (G .set (n,x)) by FUNCT_4:10; assume A2: not n in _GraphSelectors ; ::_thesis: ( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph ) then EdgeSelector <> n by ENUMSET1:def_2; then A3: not EdgeSelector in dom (n .--> x) by TARSKI:def_1; TargetSelector <> n by A2, ENUMSET1:def_2; then A4: not TargetSelector in dom (n .--> x) by TARSKI:def_1; SourceSelector <> n by A2, ENUMSET1:def_2; then A5: not SourceSelector in dom (n .--> x) by TARSKI:def_1; VertexSelector <> n by A2, ENUMSET1:def_2; then not VertexSelector in dom (n .--> x) by TARSKI:def_1; hence A6: ( the_Vertices_of (G .set (n,x)) = the_Vertices_of G & the_Edges_of (G .set (n,x)) = the_Edges_of G & the_Source_of (G .set (n,x)) = the_Source_of G & the_Target_of (G .set (n,x)) = the_Target_of G ) by A3, A5, A4, FUNCT_4:11; ::_thesis: G .set (n,x) is _Graph A7: ( SourceSelector in dom G & TargetSelector in dom G ) by Def10; ( VertexSelector in dom G & EdgeSelector in dom G ) by Def10; hence G .set (n,x) is _Graph by A7, A1, A6, Def10; ::_thesis: verum end; theorem :: GLIB_000:11 for GS being GraphStruct for x being set holds ( the_Vertices_of (GS .set (VertexSelector,x)) = x & the_Edges_of (GS .set (EdgeSelector,x)) = x & the_Source_of (GS .set (SourceSelector,x)) = x & the_Target_of (GS .set (TargetSelector,x)) = x ) by Th8; theorem :: GLIB_000:12 for GS being GraphStruct for x, y being set for n1, n2 being Nat st n1 <> n2 holds ( n1 in dom ((GS .set (n1,x)) .set (n2,y)) & n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) proof let GS be GraphStruct; ::_thesis: for x, y being set for n1, n2 being Nat st n1 <> n2 holds ( n1 in dom ((GS .set (n1,x)) .set (n2,y)) & n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) let x, y be set ; ::_thesis: for n1, n2 being Nat st n1 <> n2 holds ( n1 in dom ((GS .set (n1,x)) .set (n2,y)) & n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) let n1, n2 be Nat; ::_thesis: ( n1 <> n2 implies ( n1 in dom ((GS .set (n1,x)) .set (n2,y)) & n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) ) assume A1: n1 <> n2 ; ::_thesis: ( n1 in dom ((GS .set (n1,x)) .set (n2,y)) & n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) set G2 = GS .set (n1,x); set G3 = (GS .set (n1,x)) .set (n2,y); A2: dom ((GS .set (n1,x)) .set (n2,y)) = (dom (GS .set (n1,x))) \/ {n2} by Th7; ( dom (GS .set (n1,x)) = (dom GS) \/ {n1} & n1 in {n1} ) by Th7, TARSKI:def_1; then n1 in dom (GS .set (n1,x)) by XBOOLE_0:def_3; hence n1 in dom ((GS .set (n1,x)) .set (n2,y)) by A2, XBOOLE_0:def_3; ::_thesis: ( n2 in dom ((GS .set (n1,x)) .set (n2,y)) & ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) n2 in {n2} by TARSKI:def_1; hence n2 in dom ((GS .set (n1,x)) .set (n2,y)) by A2, XBOOLE_0:def_3; ::_thesis: ( ((GS .set (n1,x)) .set (n2,y)) . n1 = x & ((GS .set (n1,x)) .set (n2,y)) . n2 = y ) thus ((GS .set (n1,x)) .set (n2,y)) . n1 = (GS .set (n1,x)) . n1 by A1, Th9 .= x by Th8 ; ::_thesis: ((GS .set (n1,x)) .set (n2,y)) . n2 = y thus ((GS .set (n1,x)) .set (n2,y)) . n2 = y by Th8; ::_thesis: verum end; theorem :: GLIB_000:13 for G being _Graph for e, x, y being set st e Joins x,y,G holds ( x in the_Vertices_of G & y in the_Vertices_of G ) proof let G be _Graph; ::_thesis: for e, x, y being set st e Joins x,y,G holds ( x in the_Vertices_of G & y in the_Vertices_of G ) let e, x, y be set ; ::_thesis: ( e Joins x,y,G implies ( x in the_Vertices_of G & y in the_Vertices_of G ) ) assume A1: e Joins x,y,G ; ::_thesis: ( x in the_Vertices_of G & y in the_Vertices_of G ) then A2: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by Def13; e in the_Edges_of G by A1, Def13; hence ( x in the_Vertices_of G & y in the_Vertices_of G ) by A2, FUNCT_2:5; ::_thesis: verum end; theorem :: GLIB_000:14 for G being _Graph for e, x, y being set st e Joins x,y,G holds e Joins y,x,G proof let G be _Graph; ::_thesis: for e, x, y being set st e Joins x,y,G holds e Joins y,x,G let e, x, y be set ; ::_thesis: ( e Joins x,y,G implies e Joins y,x,G ) assume A1: e Joins x,y,G ; ::_thesis: e Joins y,x,G then A2: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by Def13; e in the_Edges_of G by A1, Def13; hence e Joins y,x,G by A2, Def13; ::_thesis: verum end; theorem :: GLIB_000:15 for G being _Graph for e, x1, y1, x2, y2 being set st e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) holds ( x1 = y2 & y1 = x2 ) proof let G be _Graph; ::_thesis: for e, x1, y1, x2, y2 being set st e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) holds ( x1 = y2 & y1 = x2 ) let e, x1, y1, x2, y2 be set ; ::_thesis: ( e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) implies ( x1 = y2 & y1 = x2 ) ) assume that A1: e Joins x1,y1,G and A2: e Joins x2,y2,G ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) set S = (the_Source_of G) . e; set T = (the_Target_of G) . e; now__::_thesis:_(_(_x1_=_x2_&_y1_=_y2_)_or_(_x1_=_y2_&_y1_=_x2_)_) percases ( ( (the_Source_of G) . e = x1 & (the_Target_of G) . e = y1 ) or ( (the_Source_of G) . e = y1 & (the_Target_of G) . e = x1 ) ) by A1, Def13; supposeA3: ( (the_Source_of G) . e = x1 & (the_Target_of G) . e = y1 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) now__::_thesis:_(_(_x1_=_x2_&_y1_=_y2_)_or_(_x1_=_y2_&_y1_=_x2_)_) percases ( ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) or ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ) by A2, Def13; suppose ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A3; ::_thesis: verum end; suppose ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A3; ::_thesis: verum end; end; end; hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; ::_thesis: verum end; supposeA4: ( (the_Source_of G) . e = y1 & (the_Target_of G) . e = x1 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) now__::_thesis:_(_(_x1_=_x2_&_y1_=_y2_)_or_(_x1_=_y2_&_y1_=_x2_)_) percases ( ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) or ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ) by A2, Def13; suppose ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A4; ::_thesis: verum end; suppose ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ; ::_thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A4; ::_thesis: verum end; end; end; hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; ::_thesis: verum end; end; end; hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; ::_thesis: verum end; theorem :: GLIB_000:16 for G being _Graph for e, x, y being set holds ( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) by Lm2; theorem :: GLIB_000:17 for G being _Graph for e, x, y, X, Y being set st e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) holds e SJoins X,Y,G proof let G be _Graph; ::_thesis: for e, x, y, X, Y being set st e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) holds e SJoins X,Y,G let e, x, y, X, Y be set ; ::_thesis: ( e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) implies e SJoins X,Y,G ) assume that A1: e Joins x,y,G and A2: ( ( x in X & y in Y ) or ( x in Y & y in X ) ) ; ::_thesis: e SJoins X,Y,G A3: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by A1, Def13; e in the_Edges_of G by A1, Def13; hence e SJoins X,Y,G by A2, A3, Def15; ::_thesis: verum end; theorem :: GLIB_000:18 for G being _Graph holds ( G is loopless iff for v, e being set holds not e Joins v,v,G ) proof let G be _Graph; ::_thesis: ( G is loopless iff for v, e being set holds not e Joins v,v,G ) hereby ::_thesis: ( ( for v, e being set holds not e Joins v,v,G ) implies G is loopless ) assume A1: G is loopless ; ::_thesis: for v, e being set holds not e Joins v,v,G let v be set ; ::_thesis: for e being set holds not e Joins v,v,G now__::_thesis:_for_e_being_set_holds_not_e_Joins_v,v,G given e being set such that A2: e Joins v,v,G ; ::_thesis: contradiction A3: (the_Target_of G) . e = v by A2, Def13; ( e in the_Edges_of G & (the_Source_of G) . e = v ) by A2, Def13; hence contradiction by A1, A3, Def18; ::_thesis: verum end; hence for e being set holds not e Joins v,v,G ; ::_thesis: verum end; assume A4: for v, e being set holds not e Joins v,v,G ; ::_thesis: G is loopless now__::_thesis:_for_e_being_set_holds_ (_not_e_in_the_Edges_of_G_or_not_(the_Source_of_G)_._e_=_(the_Target_of_G)_._e_) given e being set such that A5: ( e in the_Edges_of G & (the_Source_of G) . e = (the_Target_of G) . e ) ; ::_thesis: contradiction set v = (the_Source_of G) . e; e Joins (the_Source_of G) . e,(the_Source_of G) . e,G by A5, Def13; hence contradiction by A4; ::_thesis: verum end; hence G is loopless by Def18; ::_thesis: verum end; theorem :: GLIB_000:19 for G being finite loopless _Graph for v being Vertex of G holds v .degree() = card (v .edgesInOut()) proof let G be finite loopless _Graph; ::_thesis: for v being Vertex of G holds v .degree() = card (v .edgesInOut()) let v be Vertex of G; ::_thesis: v .degree() = card (v .edgesInOut()) set In = v .edgesIn() ; set Out = v .edgesOut() ; now__::_thesis:_for_e_being_set_holds_not_e_in_(v_.edgesIn())_/\_(v_.edgesOut()) given e being set such that A1: e in (v .edgesIn()) /\ (v .edgesOut()) ; ::_thesis: contradiction e in v .edgesOut() by A1, XBOOLE_0:def_4; then A2: (the_Source_of G) . e = v by Lm9; e in v .edgesIn() by A1, XBOOLE_0:def_4; then (the_Target_of G) . e = v by Lm8; hence contradiction by A1, A2, Def18; ::_thesis: verum end; then (v .edgesIn()) /\ (v .edgesOut()) = {} by XBOOLE_0:def_1; then v .edgesIn() misses v .edgesOut() by XBOOLE_0:def_7; hence v .degree() = card (v .edgesInOut()) by CARD_2:40; ::_thesis: verum end; theorem :: GLIB_000:20 for G being non trivial _Graph for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty proof let G be non trivial _Graph; ::_thesis: for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty let v be Vertex of G; ::_thesis: not (the_Vertices_of G) \ {v} is empty set VG = the_Vertices_of G; now__::_thesis:_not_(the_Vertices_of_G)_\_{v}_=_{} assume (the_Vertices_of G) \ {v} = {} ; ::_thesis: contradiction then the_Vertices_of G c= {v} by XBOOLE_1:37; then the_Vertices_of G = {v} by ZFMISC_1:33; then card (the_Vertices_of G) = 1 by CARD_1:30; hence contradiction by Def19; ::_thesis: verum end; hence not (the_Vertices_of G) \ {v} is empty ; ::_thesis: verum end; theorem :: GLIB_000:21 for G being non trivial _Graph ex v1, v2 being Vertex of G st v1 <> v2 proof let G be non trivial _Graph; ::_thesis: ex v1, v2 being Vertex of G st v1 <> v2 set VG = the_Vertices_of G; take v1 = choose (the_Vertices_of G); ::_thesis: ex v2 being Vertex of G st v1 <> v2 set VG2 = (the_Vertices_of G) \ {v1}; now__::_thesis:_not_(the_Vertices_of_G)_\_{v1}_=_{} assume A1: (the_Vertices_of G) \ {v1} = {} ; ::_thesis: contradiction card (((the_Vertices_of G) \ {v1}) \/ {v1}) = (card ((the_Vertices_of G) \ {v1})) +` (card {v1}) by CARD_2:35, XBOOLE_1:79 .= 0 +` 1 by A1, CARD_1:27, CARD_1:30 .= card (0 +^ 1) by CARD_2:def_1 .= card (0 + 1) by CARD_2:36 .= 1 by CARD_1:def_2 ; then card (the_Vertices_of G) = 1 by XBOOLE_1:45; hence contradiction by Def19; ::_thesis: verum end; then reconsider VG2 = (the_Vertices_of G) \ {v1} as non empty set ; set v2 = choose VG2; A2: not choose VG2 in {v1} by XBOOLE_0:def_5; reconsider v2 = choose VG2 as Vertex of G by XBOOLE_0:def_5; take v2 ; ::_thesis: v1 <> v2 thus v1 <> v2 by A2, TARSKI:def_1; ::_thesis: verum end; theorem Th22: :: GLIB_000:22 for G being trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v} proof let G be trivial _Graph; ::_thesis: ex v being Vertex of G st the_Vertices_of G = {v} card (the_Vertices_of G) = 1 by Def19; then consider v being set such that A1: the_Vertices_of G = {v} by CARD_2:42; reconsider v = v as Vertex of G by A1, TARSKI:def_1; take v ; ::_thesis: the_Vertices_of G = {v} thus the_Vertices_of G = {v} by A1; ::_thesis: verum end; theorem :: GLIB_000:23 for G being loopless trivial _Graph holds the_Edges_of G = {} proof let G be loopless trivial _Graph; ::_thesis: the_Edges_of G = {} consider v being Vertex of G such that A1: the_Vertices_of G = {v} by Th22; now__::_thesis:_not_the_Edges_of_G_<>_{} assume the_Edges_of G <> {} ; ::_thesis: contradiction then consider e being set such that A2: e in the_Edges_of G by XBOOLE_0:def_1; (the_Target_of G) . e in {v} by A1, A2, FUNCT_2:5; then A3: (the_Target_of G) . e = v by TARSKI:def_1; (the_Source_of G) . e in {v} by A1, A2, FUNCT_2:5; then (the_Source_of G) . e = v by TARSKI:def_1; hence contradiction by A2, A3, Def18; ::_thesis: verum end; hence the_Edges_of G = {} ; ::_thesis: verum end; theorem :: GLIB_000:24 for G being _Graph st the_Edges_of G = {} holds G is simple proof let G be _Graph; ::_thesis: ( the_Edges_of G = {} implies G is simple ) assume A1: the_Edges_of G = {} ; ::_thesis: G is simple then for e being set holds ( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) ; then A2: G is loopless by Def18; for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds e1 = e2 by A1, Def13; then G is non-multi by Def20; hence G is simple by A2; ::_thesis: verum end; theorem :: GLIB_000:25 for G being finite _Graph holds G .order() >= 1 proof let G be finite _Graph; ::_thesis: G .order() >= 1 0 + 1 < (G .order()) + 1 by NAT_1:3, XREAL_1:8; hence G .order() >= 1 by NAT_1:13; ::_thesis: verum end; theorem :: GLIB_000:26 for G being finite _Graph holds ( G .order() = 1 iff G is trivial ) by Def19; theorem :: GLIB_000:27 for G being finite _Graph holds ( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} ) proof let G be finite _Graph; ::_thesis: ( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} ) hereby ::_thesis: ( ex v being Vertex of G st the_Vertices_of G = {v} implies G .order() = 1 ) assume G .order() = 1 ; ::_thesis: ex v being Vertex of G st the_Vertices_of G = {v} then consider v being set such that A1: the_Vertices_of G = {v} by CARD_2:42; reconsider v = v as Vertex of G by A1, TARSKI:def_1; take v = v; ::_thesis: the_Vertices_of G = {v} thus the_Vertices_of G = {v} by A1; ::_thesis: verum end; given v being Vertex of G such that A2: the_Vertices_of G = {v} ; ::_thesis: G .order() = 1 thus G .order() = 1 by A2, CARD_1:30; ::_thesis: verum end; theorem Th28: :: GLIB_000:28 for G being _Graph for e, X being set holds ( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X ) proof let G be _Graph; ::_thesis: for e, X being set holds ( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X ) let e, X be set ; ::_thesis: ( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X ) hereby ::_thesis: ( e in G .edgesInOut X implies ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) ) assume that A1: e in the_Edges_of G and A2: ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ; ::_thesis: e in G .edgesInOut X now__::_thesis:_e_in_G_.edgesInOut_X percases ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) by A2; suppose (the_Source_of G) . e in X ; ::_thesis: e in G .edgesInOut X then e in G .edgesOutOf X by A1, Def27; hence e in G .edgesInOut X by XBOOLE_0:def_3; ::_thesis: verum end; suppose (the_Target_of G) . e in X ; ::_thesis: e in G .edgesInOut X then e in G .edgesInto X by A1, Def26; hence e in G .edgesInOut X by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence e in G .edgesInOut X ; ::_thesis: verum end; assume e in G .edgesInOut X ; ::_thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) then ( e in G .edgesInto X or e in G .edgesOutOf X ) by XBOOLE_0:def_3; hence ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) by Def26, Def27; ::_thesis: verum end; theorem :: GLIB_000:29 for G being _Graph for X being set holds ( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X ) proof let G be _Graph; ::_thesis: for X being set holds ( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X ) let X be set ; ::_thesis: ( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X ) for z being set st z in G .edgesInto X holds z in G .edgesInOut X by XBOOLE_0:def_3; hence G .edgesInto X c= G .edgesInOut X by TARSKI:def_3; ::_thesis: G .edgesOutOf X c= G .edgesInOut X for z being set st z in G .edgesOutOf X holds z in G .edgesInOut X by XBOOLE_0:def_3; hence G .edgesOutOf X c= G .edgesInOut X by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:30 for G being _Graph holds the_Edges_of G = G .edgesInOut (the_Vertices_of G) proof let G be _Graph; ::_thesis: the_Edges_of G = G .edgesInOut (the_Vertices_of G) set EG = the_Edges_of G; set SG = the_Source_of G; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_Edges_of_G_implies_x_in_G_.edgesInOut_(the_Vertices_of_G)_)_&_(_x_in_G_.edgesInOut_(the_Vertices_of_G)_implies_x_in_the_Edges_of_G_)_) let x be set ; ::_thesis: ( ( x in the_Edges_of G implies x in G .edgesInOut (the_Vertices_of G) ) & ( x in G .edgesInOut (the_Vertices_of G) implies x in the_Edges_of G ) ) hereby ::_thesis: ( x in G .edgesInOut (the_Vertices_of G) implies x in the_Edges_of G ) assume A1: x in the_Edges_of G ; ::_thesis: x in G .edgesInOut (the_Vertices_of G) then (the_Source_of G) . x in the_Vertices_of G by FUNCT_2:5; hence x in G .edgesInOut (the_Vertices_of G) by A1, Th28; ::_thesis: verum end; assume x in G .edgesInOut (the_Vertices_of G) ; ::_thesis: x in the_Edges_of G hence x in the_Edges_of G ; ::_thesis: verum end; hence the_Edges_of G = G .edgesInOut (the_Vertices_of G) by TARSKI:1; ::_thesis: verum end; theorem :: GLIB_000:31 for G being _Graph for e, X being set holds ( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X ) by Lm6; theorem :: GLIB_000:32 for G being _Graph for x, X, y, e being set st x in X & y in X & e Joins x,y,G holds e in G .edgesBetween X proof let G be _Graph; ::_thesis: for x, X, y, e being set st x in X & y in X & e Joins x,y,G holds e in G .edgesBetween X let x, X, y, e be set ; ::_thesis: ( x in X & y in X & e Joins x,y,G implies e in G .edgesBetween X ) assume that A1: ( x in X & y in X ) and A2: e Joins x,y,G ; ::_thesis: e in G .edgesBetween X A3: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by A2, Def13; e in the_Edges_of G by A2, Def13; hence e in G .edgesBetween X by A1, A3, Lm6; ::_thesis: verum end; theorem :: GLIB_000:33 for G being _Graph for X being set holds G .edgesBetween X c= G .edgesInOut X proof let G be _Graph; ::_thesis: for X being set holds G .edgesBetween X c= G .edgesInOut X let X be set ; ::_thesis: G .edgesBetween X c= G .edgesInOut X now__::_thesis:_for_z_being_set_st_z_in_G_.edgesBetween_X_holds_ z_in_G_.edgesInOut_X let z be set ; ::_thesis: ( z in G .edgesBetween X implies z in G .edgesInOut X ) assume z in G .edgesBetween X ; ::_thesis: z in G .edgesInOut X then z in G .edgesInto X by XBOOLE_0:def_4; hence z in G .edgesInOut X by XBOOLE_0:def_3; ::_thesis: verum end; hence G .edgesBetween X c= G .edgesInOut X by TARSKI:def_3; ::_thesis: verum end; theorem Th34: :: GLIB_000:34 for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G) proof let G be _Graph; ::_thesis: the_Edges_of G = G .edgesBetween (the_Vertices_of G) set EG = the_Edges_of G; set SG = the_Source_of G; set TG = the_Target_of G; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_Edges_of_G_implies_x_in_G_.edgesBetween_(the_Vertices_of_G)_)_&_(_x_in_G_.edgesBetween_(the_Vertices_of_G)_implies_x_in_the_Edges_of_G_)_) let x be set ; ::_thesis: ( ( x in the_Edges_of G implies x in G .edgesBetween (the_Vertices_of G) ) & ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G ) ) hereby ::_thesis: ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G ) assume A1: x in the_Edges_of G ; ::_thesis: x in G .edgesBetween (the_Vertices_of G) then ( (the_Source_of G) . x in the_Vertices_of G & (the_Target_of G) . x in the_Vertices_of G ) by FUNCT_2:5; hence x in G .edgesBetween (the_Vertices_of G) by A1, Lm6; ::_thesis: verum end; assume x in G .edgesBetween (the_Vertices_of G) ; ::_thesis: x in the_Edges_of G hence x in the_Edges_of G ; ::_thesis: verum end; hence the_Edges_of G = G .edgesBetween (the_Vertices_of G) by TARSKI:1; ::_thesis: verum end; theorem Th35: :: GLIB_000:35 for G being _Graph for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X) proof let G be _Graph; ::_thesis: for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X) let X be set ; ::_thesis: (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X) set EG = the_Edges_of G; set VG = the_Vertices_of G; set EIO = G .edgesInOut X; set EB = G .edgesBetween ((the_Vertices_of G) \ X); now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(the_Edges_of_G)_\_(G_.edgesInOut_X)_implies_x_in_G_.edgesBetween_((the_Vertices_of_G)_\_X)_)_&_(_x_in_G_.edgesBetween_((the_Vertices_of_G)_\_X)_implies_x_in_(the_Edges_of_G)_\_(G_.edgesInOut_X)_)_) let x be set ; ::_thesis: ( ( x in (the_Edges_of G) \ (G .edgesInOut X) implies x in G .edgesBetween ((the_Vertices_of G) \ X) ) & ( x in G .edgesBetween ((the_Vertices_of G) \ X) implies x in (the_Edges_of G) \ (G .edgesInOut X) ) ) hereby ::_thesis: ( x in G .edgesBetween ((the_Vertices_of G) \ X) implies x in (the_Edges_of G) \ (G .edgesInOut X) ) assume A1: x in (the_Edges_of G) \ (G .edgesInOut X) ; ::_thesis: x in G .edgesBetween ((the_Vertices_of G) \ X) then A2: (the_Target_of G) . x in the_Vertices_of G by FUNCT_2:5; A3: not x in G .edgesInOut X by A1, XBOOLE_0:def_5; then not (the_Target_of G) . x in X by A1, Th28; then A4: (the_Target_of G) . x in (the_Vertices_of G) \ X by A2, XBOOLE_0:def_5; A5: (the_Source_of G) . x in the_Vertices_of G by A1, FUNCT_2:5; not (the_Source_of G) . x in X by A1, A3, Th28; then (the_Source_of G) . x in (the_Vertices_of G) \ X by A5, XBOOLE_0:def_5; hence x in G .edgesBetween ((the_Vertices_of G) \ X) by A1, A4, Lm6; ::_thesis: verum end; assume A6: x in G .edgesBetween ((the_Vertices_of G) \ X) ; ::_thesis: x in (the_Edges_of G) \ (G .edgesInOut X) then (the_Target_of G) . x in (the_Vertices_of G) \ X by Lm6; then A7: not (the_Target_of G) . x in X by XBOOLE_0:def_5; (the_Source_of G) . x in (the_Vertices_of G) \ X by A6, Lm6; then not (the_Source_of G) . x in X by XBOOLE_0:def_5; then not x in G .edgesInOut X by A7, Th28; hence x in (the_Edges_of G) \ (G .edgesInOut X) by A6, XBOOLE_0:def_5; ::_thesis: verum end; hence (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X) by TARSKI:1; ::_thesis: verum end; theorem :: GLIB_000:36 for G being _Graph for X, Y being set st X c= Y holds G .edgesBetween X c= G .edgesBetween Y proof let G be _Graph; ::_thesis: for X, Y being set st X c= Y holds G .edgesBetween X c= G .edgesBetween Y let X, Y be set ; ::_thesis: ( X c= Y implies G .edgesBetween X c= G .edgesBetween Y ) assume A1: X c= Y ; ::_thesis: G .edgesBetween X c= G .edgesBetween Y now__::_thesis:_for_x_being_set_st_x_in_G_.edgesBetween_X_holds_ x_in_G_.edgesBetween_Y let x be set ; ::_thesis: ( x in G .edgesBetween X implies x in G .edgesBetween Y ) assume A2: x in G .edgesBetween X ; ::_thesis: x in G .edgesBetween Y then ( (the_Source_of G) . x in X & (the_Target_of G) . x in X ) by Lm6; hence x in G .edgesBetween Y by A1, A2, Lm6; ::_thesis: verum end; hence G .edgesBetween X c= G .edgesBetween Y by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:37 for G being _Graph for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) proof let G be _Graph; ::_thesis: for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) let X1, X2, Y1, Y2 be set ; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) ) assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) now__::_thesis:_for_e_being_set_st_e_in_G_.edgesBetween_(X1,Y1)_holds_ e_in_G_.edgesBetween_(X2,Y2) let e be set ; ::_thesis: ( e in G .edgesBetween (X1,Y1) implies e in G .edgesBetween (X2,Y2) ) assume A2: e in G .edgesBetween (X1,Y1) ; ::_thesis: e in G .edgesBetween (X2,Y2) then e SJoins X1,Y1,G by Def30; then ( ( (the_Source_of G) . e in X1 & (the_Target_of G) . e in Y1 ) or ( (the_Source_of G) . e in Y1 & (the_Target_of G) . e in X1 ) ) by Def15; then e SJoins X2,Y2,G by A1, A2, Def15; hence e in G .edgesBetween (X2,Y2) by Def30; ::_thesis: verum end; hence G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:38 for G being _Graph for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) proof let G be _Graph; ::_thesis: for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) let X1, X2, Y1, Y2 be set ; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) ) assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) now__::_thesis:_for_e_being_set_st_e_in_G_.edgesDBetween_(X1,Y1)_holds_ e_in_G_.edgesDBetween_(X2,Y2) let e be set ; ::_thesis: ( e in G .edgesDBetween (X1,Y1) implies e in G .edgesDBetween (X2,Y2) ) assume A2: e in G .edgesDBetween (X1,Y1) ; ::_thesis: e in G .edgesDBetween (X2,Y2) then e DSJoins X1,Y1,G by Def31; then ( (the_Source_of G) . e in X1 & (the_Target_of G) . e in Y1 ) by Def16; then e DSJoins X2,Y2,G by A1, A2, Def16; hence e in G .edgesDBetween (X2,Y2) by Def31; ::_thesis: verum end; hence G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:39 for G being _Graph for v being Vertex of G holds ( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) & v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) ) proof let G be _Graph; ::_thesis: for v being Vertex of G holds ( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) & v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) ) let v be Vertex of G; ::_thesis: ( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) & v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) ) now__::_thesis:_for_e_being_set_holds_ (_(_e_in_v_.edgesIn()_implies_e_in_G_.edgesDBetween_((the_Vertices_of_G),{v})_)_&_(_e_in_G_.edgesDBetween_((the_Vertices_of_G),{v})_implies_e_in_v_.edgesIn()_)_) let e be set ; ::_thesis: ( ( e in v .edgesIn() implies e in G .edgesDBetween ((the_Vertices_of G),{v}) ) & ( e in G .edgesDBetween ((the_Vertices_of G),{v}) implies e in v .edgesIn() ) ) hereby ::_thesis: ( e in G .edgesDBetween ((the_Vertices_of G),{v}) implies e in v .edgesIn() ) assume A1: e in v .edgesIn() ; ::_thesis: e in G .edgesDBetween ((the_Vertices_of G),{v}) then (the_Target_of G) . e = v by Lm8; then A2: (the_Target_of G) . e in {v} by TARSKI:def_1; (the_Source_of G) . e in the_Vertices_of G by A1, FUNCT_2:5; then e DSJoins the_Vertices_of G,{v},G by A1, A2, Def16; hence e in G .edgesDBetween ((the_Vertices_of G),{v}) by Def31; ::_thesis: verum end; assume A3: e in G .edgesDBetween ((the_Vertices_of G),{v}) ; ::_thesis: e in v .edgesIn() then e DSJoins the_Vertices_of G,{v},G by Def31; then (the_Target_of G) . e in {v} by Def16; then (the_Target_of G) . e = v by TARSKI:def_1; hence e in v .edgesIn() by A3, Lm8; ::_thesis: verum end; hence v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) by TARSKI:1; ::_thesis: v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) now__::_thesis:_for_e_being_set_holds_ (_(_e_in_v_.edgesOut()_implies_e_in_G_.edgesDBetween_({v},(the_Vertices_of_G))_)_&_(_e_in_G_.edgesDBetween_({v},(the_Vertices_of_G))_implies_e_in_v_.edgesOut()_)_) let e be set ; ::_thesis: ( ( e in v .edgesOut() implies e in G .edgesDBetween ({v},(the_Vertices_of G)) ) & ( e in G .edgesDBetween ({v},(the_Vertices_of G)) implies e in v .edgesOut() ) ) hereby ::_thesis: ( e in G .edgesDBetween ({v},(the_Vertices_of G)) implies e in v .edgesOut() ) assume A4: e in v .edgesOut() ; ::_thesis: e in G .edgesDBetween ({v},(the_Vertices_of G)) then (the_Source_of G) . e = v by Lm9; then A5: (the_Source_of G) . e in {v} by TARSKI:def_1; (the_Target_of G) . e in the_Vertices_of G by A4, FUNCT_2:5; then e DSJoins {v}, the_Vertices_of G,G by A4, A5, Def16; hence e in G .edgesDBetween ({v},(the_Vertices_of G)) by Def31; ::_thesis: verum end; assume A6: e in G .edgesDBetween ({v},(the_Vertices_of G)) ; ::_thesis: e in v .edgesOut() then e DSJoins {v}, the_Vertices_of G,G by Def31; then (the_Source_of G) . e in {v} by Def16; then (the_Source_of G) . e = v by TARSKI:def_1; hence e in v .edgesOut() by A6, Lm9; ::_thesis: verum end; hence v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) by TARSKI:1; ::_thesis: verum end; theorem :: GLIB_000:40 for G being _Graph holds G is Subgraph of G by Lm4; theorem Th41: :: GLIB_000:41 for G1, G2 being _Graph holds ( G1 is Subgraph of G2 & G2 is Subgraph of G1 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ) proof let G1, G2 be _Graph; ::_thesis: ( G1 is Subgraph of G2 & G2 is Subgraph of G1 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ) hereby ::_thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 implies ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) assume that A1: G1 is Subgraph of G2 and A2: G2 is Subgraph of G1 ; ::_thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) A3: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 ) by A2, Def32; ( the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 ) by A1, Def32; hence A4: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A3, XBOOLE_0:def_10; ::_thesis: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) then A5: ( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G1 ) by FUNCT_2:def_1; for e being set st e in dom (the_Source_of G1) holds (the_Source_of G1) . e = (the_Source_of G2) . e by A1, Def32; hence the_Source_of G1 = the_Source_of G2 by A5, FUNCT_1:2; ::_thesis: the_Target_of G1 = the_Target_of G2 A6: ( dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) = the_Edges_of G1 ) by A4, FUNCT_2:def_1; for e being set st e in dom (the_Target_of G1) holds (the_Target_of G1) . e = (the_Target_of G2) . e by A1, Def32; hence the_Target_of G1 = the_Target_of G2 by A6, FUNCT_1:2; ::_thesis: verum end; assume that A7: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) and A8: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ; ::_thesis: ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) for e being set st e in the_Edges_of G1 holds ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by A8; hence ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by A7, Def32; ::_thesis: verum end; theorem :: GLIB_000:42 for G1 being _Graph for G2 being Subgraph of G1 for x being set holds ( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) ; theorem Th43: :: GLIB_000:43 for G1 being _Graph for G2 being Subgraph of G1 for G3 being Subgraph of G2 holds G3 is Subgraph of G1 proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for G3 being Subgraph of G2 holds G3 is Subgraph of G1 let G2 be Subgraph of G1; ::_thesis: for G3 being Subgraph of G2 holds G3 is Subgraph of G1 let G3 be Subgraph of G2; ::_thesis: G3 is Subgraph of G1 A1: the_Edges_of G2 c= the_Edges_of G1 ; A2: the_Vertices_of G3 c= the_Vertices_of G2 ; now__::_thesis:_(_the_Vertices_of_G3_c=_the_Vertices_of_G1_&_the_Edges_of_G3_c=_the_Edges_of_G1_&_(_for_e_being_set_st_e_in_the_Edges_of_G3_holds_ (_(the_Source_of_G3)_._e_=_(the_Source_of_G1)_._e_&_(the_Target_of_G3)_._e_=_(the_Target_of_G1)_._e_)_)_) thus the_Vertices_of G3 c= the_Vertices_of G1 by A2, XBOOLE_1:1; ::_thesis: ( the_Edges_of G3 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G3 holds ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) ) ) thus the_Edges_of G3 c= the_Edges_of G1 by A1, XBOOLE_1:1; ::_thesis: for e being set st e in the_Edges_of G3 holds ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) let e be set ; ::_thesis: ( e in the_Edges_of G3 implies ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) ) assume A3: e in the_Edges_of G3 ; ::_thesis: ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) hence (the_Source_of G3) . e = (the_Source_of G2) . e by Def32 .= (the_Source_of G1) . e by A3, Def32 ; ::_thesis: (the_Target_of G3) . e = (the_Target_of G1) . e thus (the_Target_of G3) . e = (the_Target_of G2) . e by A3, Def32 .= (the_Target_of G1) . e by A3, Def32 ; ::_thesis: verum end; hence G3 is Subgraph of G1 by Def32; ::_thesis: verum end; theorem Th44: :: GLIB_000:44 for G being _Graph for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 holds G1 is Subgraph of G2 proof let G be _Graph; ::_thesis: for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 holds G1 is Subgraph of G2 let G1, G2 be Subgraph of G; ::_thesis: ( the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 implies G1 is Subgraph of G2 ) assume that A1: the_Vertices_of G1 c= the_Vertices_of G2 and A2: the_Edges_of G1 c= the_Edges_of G2 ; ::_thesis: G1 is Subgraph of G2 now__::_thesis:_for_e_being_set_st_e_in_the_Edges_of_G1_holds_ (_(the_Source_of_G1)_._e_=_(the_Source_of_G2)_._e_&_(the_Target_of_G1)_._e_=_(the_Target_of_G2)_._e_) let e be set ; ::_thesis: ( e in the_Edges_of G1 implies ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) ) assume A3: e in the_Edges_of G1 ; ::_thesis: ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) hence (the_Source_of G1) . e = (the_Source_of G) . e by Def32 .= (the_Source_of G2) . e by A2, A3, Def32 ; ::_thesis: (the_Target_of G1) . e = (the_Target_of G2) . e thus (the_Target_of G1) . e = (the_Target_of G) . e by A3, Def32 .= (the_Target_of G2) . e by A2, A3, Def32 ; ::_thesis: verum end; hence G1 is Subgraph of G2 by A1, A2, Def32; ::_thesis: verum end; theorem Th45: :: GLIB_000:45 for G1 being _Graph for G2 being Subgraph of G1 holds ( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 holds ( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) ) let G2 be Subgraph of G1; ::_thesis: ( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) ) set S2 = (the_Source_of G1) | (the_Edges_of G2); set T2 = (the_Target_of G1) | (the_Edges_of G2); A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_Source_of_G2)_holds_ (the_Source_of_G2)_._x_=_((the_Source_of_G1)_|_(the_Edges_of_G2))_._x let x be set ; ::_thesis: ( x in dom (the_Source_of G2) implies (the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x ) assume A2: x in dom (the_Source_of G2) ; ::_thesis: (the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x hence (the_Source_of G2) . x = (the_Source_of G1) . x by Def32 .= ((the_Source_of G1) | (the_Edges_of G2)) . x by A2, FUNCT_1:49 ; ::_thesis: verum end; dom (the_Source_of G1) = the_Edges_of G1 by FUNCT_2:def_1; then ( dom (the_Source_of G2) = the_Edges_of G2 & dom ((the_Source_of G1) | (the_Edges_of G2)) = the_Edges_of G2 ) by FUNCT_2:def_1, RELAT_1:62; hence the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) by A1, FUNCT_1:2; ::_thesis: the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_Target_of_G2)_holds_ (the_Target_of_G2)_._x_=_((the_Target_of_G1)_|_(the_Edges_of_G2))_._x let x be set ; ::_thesis: ( x in dom (the_Target_of G2) implies (the_Target_of G2) . x = ((the_Target_of G1) | (the_Edges_of G2)) . x ) assume A4: x in dom (the_Target_of G2) ; ::_thesis: (the_Target_of G2) . x = ((the_Target_of G1) | (the_Edges_of G2)) . x hence (the_Target_of G2) . x = (the_Target_of G1) . x by Def32 .= ((the_Target_of G1) | (the_Edges_of G2)) . x by A4, FUNCT_1:49 ; ::_thesis: verum end; dom (the_Target_of G1) = the_Edges_of G1 by FUNCT_2:def_1; then ( dom (the_Target_of G2) = the_Edges_of G2 & dom ((the_Target_of G1) | (the_Edges_of G2)) = the_Edges_of G2 ) by FUNCT_2:def_1, RELAT_1:62; hence the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) by A3, FUNCT_1:2; ::_thesis: verum end; theorem :: GLIB_000:46 for G being _Graph for V1, V2, E1, E2 being set for G1 being inducedSubgraph of G,V1,E1 for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds G2 is Subgraph of G1 proof let G be _Graph; ::_thesis: for V1, V2, E1, E2 being set for G1 being inducedSubgraph of G,V1,E1 for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds G2 is Subgraph of G1 let V1, V2, E1, E2 be set ; ::_thesis: for G1 being inducedSubgraph of G,V1,E1 for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds G2 is Subgraph of G1 let G1 be inducedSubgraph of G,V1,E1; ::_thesis: for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds G2 is Subgraph of G1 let G2 be inducedSubgraph of G,V2,E2; ::_thesis: ( V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 implies G2 is Subgraph of G1 ) assume that A1: ( V2 c= V1 & E2 c= E1 ) and A2: ( V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 ) ; ::_thesis: G2 is Subgraph of G1 A3: ( the_Vertices_of G2 = V2 & the_Edges_of G2 = E2 ) by A2, Def37; now__::_thesis:_G2_is_Subgraph_of_G1 percases ( ( V1 is non empty Subset of (the_Vertices_of G) & E1 c= G .edgesBetween V1 ) or not V1 is non empty Subset of (the_Vertices_of G) or not E1 c= G .edgesBetween V1 ) ; suppose ( V1 is non empty Subset of (the_Vertices_of G) & E1 c= G .edgesBetween V1 ) ; ::_thesis: G2 is Subgraph of G1 then ( the_Vertices_of G1 = V1 & the_Edges_of G1 = E1 ) by Def37; hence G2 is Subgraph of G1 by A1, A3, Th44; ::_thesis: verum end; suppose ( not V1 is non empty Subset of (the_Vertices_of G) or not E1 c= G .edgesBetween V1 ) ; ::_thesis: G2 is Subgraph of G1 then G1 == G by Def37; then ( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G ) by Def34; hence G2 is Subgraph of G1 by A3, Th44; ::_thesis: verum end; end; end; hence G2 is Subgraph of G1 ; ::_thesis: verum end; theorem Th47: :: GLIB_000:47 for G1 being non trivial _Graph for v being Vertex of G1 for G2 being removeVertex of G1,v holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) proof let G1 be non trivial _Graph; ::_thesis: for v being Vertex of G1 for G2 being removeVertex of G1,v holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) let v be Vertex of G1; ::_thesis: for G2 being removeVertex of G1,v holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) let G2 be removeVertex of G1,v; ::_thesis: ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) set VG = the_Vertices_of G1; set V = (the_Vertices_of G1) \ {v}; now__::_thesis:_not_(the_Vertices_of_G1)_\_{v}_is_empty assume (the_Vertices_of G1) \ {v} is empty ; ::_thesis: contradiction then the_Vertices_of G1 c= {v} by XBOOLE_1:37; then the_Vertices_of G1 = {v} by ZFMISC_1:33; then card (the_Vertices_of G1) = 1 by CARD_1:30; hence contradiction by Def19; ::_thesis: verum end; then reconsider V = (the_Vertices_of G1) \ {v} as non empty Subset of (the_Vertices_of G1) ; G2 is inducedSubgraph of G1,V ; hence ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) by Def37; ::_thesis: verum end; theorem :: GLIB_000:48 for G1 being finite non trivial _Graph for v being Vertex of G1 for G2 being removeVertex of G1,v holds ( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() ) proof let G1 be finite non trivial _Graph; ::_thesis: for v being Vertex of G1 for G2 being removeVertex of G1,v holds ( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() ) let v be Vertex of G1; ::_thesis: for G2 being removeVertex of G1,v holds ( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() ) let G2 be removeVertex of G1,v; ::_thesis: ( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() ) set VG1 = the_Vertices_of G1; set VG2 = the_Vertices_of G2; set EG1 = the_Edges_of G1; set EG2 = the_Edges_of G2; set EV = v .edgesInOut() ; A1: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by Th47; v in {v} by TARSKI:def_1; then not v in the_Vertices_of G2 by A1, XBOOLE_0:def_5; then card (((the_Vertices_of G1) \ {v}) \/ {v}) = (G2 .order()) + 1 by A1, CARD_2:41; hence (G2 .order()) + 1 = G1 .order() by XBOOLE_1:45; ::_thesis: (G2 .size()) + (card (v .edgesInOut())) = G1 .size() A2: ( the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) & G1 .edgesBetween ((the_Vertices_of G1) \ {v}) = (the_Edges_of G1) \ (v .edgesInOut()) ) by Th35, Th47; then the_Edges_of G1 = (the_Edges_of G2) \/ (v .edgesInOut()) by XBOOLE_1:45; hence (G2 .size()) + (card (v .edgesInOut())) = G1 .size() by A2, CARD_2:40, XBOOLE_1:79; ::_thesis: verum end; theorem Th49: :: GLIB_000:49 for G1 being _Graph for V being set for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) proof let G1 be _Graph; ::_thesis: for V being set for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) let V be set ; ::_thesis: for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) let G2 be removeVertices of G1,V; ::_thesis: ( V c< the_Vertices_of G1 implies ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) ) set VG2 = (the_Vertices_of G1) \ V; assume A1: V c< the_Vertices_of G1 ; ::_thesis: ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) now__::_thesis:_not_(the_Vertices_of_G1)_\_V_is_empty assume (the_Vertices_of G1) \ V is empty ; ::_thesis: contradiction then the_Vertices_of G1 c= V by XBOOLE_1:37; hence contradiction by A1, XBOOLE_0:def_8; ::_thesis: verum end; then reconsider VG2 = (the_Vertices_of G1) \ V as non empty Subset of (the_Vertices_of G1) ; G2 is inducedSubgraph of G1,VG2 ; hence ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) by Def37; ::_thesis: verum end; theorem :: GLIB_000:50 for G1 being finite _Graph for V being Subset of (the_Vertices_of G1) for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) proof let G1 be finite _Graph; ::_thesis: for V being Subset of (the_Vertices_of G1) for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) let V be Subset of (the_Vertices_of G1); ::_thesis: for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) let G2 be removeVertices of G1,V; ::_thesis: ( V <> the_Vertices_of G1 implies ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) ) set VG1 = the_Vertices_of G1; set VG2 = the_Vertices_of G2; set EG1 = the_Edges_of G1; set EG2 = the_Edges_of G2; A1: G1 .edgesBetween ((the_Vertices_of G1) \ V) = (the_Edges_of G1) \ (G1 .edgesInOut V) by Th35; assume V <> the_Vertices_of G1 ; ::_thesis: ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) then A2: V c< the_Vertices_of G1 by XBOOLE_0:def_8; then A3: the_Vertices_of G2 = (the_Vertices_of G1) \ V by Th49; then card ((the_Vertices_of G2) \/ V) = (card (the_Vertices_of G2)) + (card V) by CARD_2:40, XBOOLE_1:79; hence (G2 .order()) + (card V) = G1 .order() by A3, XBOOLE_1:45; ::_thesis: (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() A4: the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) by A2, Th49; then the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesInOut V) by A1, XBOOLE_1:45; hence (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() by A4, A1, CARD_2:40, XBOOLE_1:79; ::_thesis: verum end; theorem Th51: :: GLIB_000:51 for G1 being _Graph for e being set for G2 being removeEdge of G1,e holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) proof let G1 be _Graph; ::_thesis: for e being set for G2 being removeEdge of G1,e holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) let e be set ; ::_thesis: for G2 being removeEdge of G1,e holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) let G2 be removeEdge of G1,e; ::_thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) set V = the_Vertices_of G1; the_Vertices_of G1 c= the_Vertices_of G1 ; then reconsider V = the_Vertices_of G1 as non empty Subset of (the_Vertices_of G1) ; set E = (the_Edges_of G1) \ {e}; reconsider E = (the_Edges_of G1) \ {e} as Subset of (G1 .edgesBetween V) by Th34; G2 is inducedSubgraph of G1,V,E ; hence ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) by Def37; ::_thesis: verum end; theorem :: GLIB_000:52 for G1 being finite _Graph for e being set for G2 being removeEdge of G1,e holds ( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) ) proof let G1 be finite _Graph; ::_thesis: for e being set for G2 being removeEdge of G1,e holds ( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) ) let e be set ; ::_thesis: for G2 being removeEdge of G1,e holds ( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) ) let G2 be removeEdge of G1,e; ::_thesis: ( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) ) A1: the_Edges_of G2 = (the_Edges_of G1) \ {e} by Th51; thus G1 .order() = G2 .order() by Th51; ::_thesis: ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) assume e in the_Edges_of G1 ; ::_thesis: (G2 .size()) + 1 = G1 .size() then for x being set st x in {e} holds x in the_Edges_of G1 by TARSKI:def_1; then {e} c= the_Edges_of G1 by TARSKI:def_3; then A2: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, XBOOLE_1:45; e in {e} by TARSKI:def_1; then not e in the_Edges_of G2 by A1, XBOOLE_0:def_5; hence (G2 .size()) + 1 = G1 .size() by A2, CARD_2:41; ::_thesis: verum end; theorem Th53: :: GLIB_000:53 for G1 being _Graph for E being set for G2 being removeEdges of G1,E holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) proof let G1 be _Graph; ::_thesis: for E being set for G2 being removeEdges of G1,E holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) let E be set ; ::_thesis: for G2 being removeEdges of G1,E holds ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) let G2 be removeEdges of G1,E; ::_thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) set V = the_Vertices_of G1; the_Vertices_of G1 c= the_Vertices_of G1 ; then reconsider V = the_Vertices_of G1 as non empty Subset of (the_Vertices_of G1) ; set E2 = (the_Edges_of G1) \ E; reconsider E2 = (the_Edges_of G1) \ E as Subset of (G1 .edgesBetween V) by Th34; G2 is inducedSubgraph of G1,V,E2 ; hence ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) by Def37; ::_thesis: verum end; theorem :: GLIB_000:54 for G1 being finite _Graph for E being set for G2 being removeEdges of G1,E holds G1 .order() = G2 .order() by Th53; theorem :: GLIB_000:55 for G1 being finite _Graph for E being Subset of (the_Edges_of G1) for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size() proof let G1 be finite _Graph; ::_thesis: for E being Subset of (the_Edges_of G1) for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size() let E be Subset of (the_Edges_of G1); ::_thesis: for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size() let G2 be removeEdges of G1,E; ::_thesis: (G2 .size()) + (card E) = G1 .size() A1: the_Edges_of G2 = (the_Edges_of G1) \ E by Th53; then the_Edges_of G1 = (the_Edges_of G2) \/ E by XBOOLE_1:45; hence (G2 .size()) + (card E) = G1 .size() by A1, CARD_2:40, XBOOLE_1:79; ::_thesis: verum end; theorem :: GLIB_000:56 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) by Lm8; theorem :: GLIB_000:57 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesIn() iff ex x being set st e DJoins x,v,G ) proof let G be _Graph; ::_thesis: for e being set for v being Vertex of G holds ( e in v .edgesIn() iff ex x being set st e DJoins x,v,G ) let e be set ; ::_thesis: for v being Vertex of G holds ( e in v .edgesIn() iff ex x being set st e DJoins x,v,G ) let v be Vertex of G; ::_thesis: ( e in v .edgesIn() iff ex x being set st e DJoins x,v,G ) hereby ::_thesis: ( ex x being set st e DJoins x,v,G implies e in v .edgesIn() ) set x = (the_Source_of G) . e; assume A1: e in v .edgesIn() ; ::_thesis: ex x being set st e DJoins x,v,G take x = (the_Source_of G) . e; ::_thesis: e DJoins x,v,G (the_Target_of G) . e = v by A1, Lm8; hence e DJoins x,v,G by A1, Def14; ::_thesis: verum end; given x being set such that A2: e DJoins x,v,G ; ::_thesis: e in v .edgesIn() ( e in the_Edges_of G & (the_Target_of G) . e = v ) by A2, Def14; hence e in v .edgesIn() by Lm8; ::_thesis: verum end; theorem :: GLIB_000:58 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) by Lm9; theorem :: GLIB_000:59 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesOut() iff ex x being set st e DJoins v,x,G ) proof let G be _Graph; ::_thesis: for e being set for v being Vertex of G holds ( e in v .edgesOut() iff ex x being set st e DJoins v,x,G ) let e be set ; ::_thesis: for v being Vertex of G holds ( e in v .edgesOut() iff ex x being set st e DJoins v,x,G ) let v be Vertex of G; ::_thesis: ( e in v .edgesOut() iff ex x being set st e DJoins v,x,G ) hereby ::_thesis: ( ex x being set st e DJoins v,x,G implies e in v .edgesOut() ) set x = (the_Target_of G) . e; assume A1: e in v .edgesOut() ; ::_thesis: ex x being set st e DJoins v,x,G take x = (the_Target_of G) . e; ::_thesis: e DJoins v,x,G (the_Source_of G) . e = v by A1, Lm9; hence e DJoins v,x,G by A1, Def14; ::_thesis: verum end; given x being set such that A2: e DJoins v,x,G ; ::_thesis: e in v .edgesOut() ( e in the_Edges_of G & (the_Source_of G) . e = v ) by A2, Def14; hence e in v .edgesOut() by Lm9; ::_thesis: verum end; theorem :: GLIB_000:60 for G being _Graph for v being Vertex of G holds v .edgesInOut() = (v .edgesIn()) \/ (v .edgesOut()) ; theorem Th61: :: GLIB_000:61 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ) proof let G be _Graph; ::_thesis: for e being set for v being Vertex of G holds ( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ) let e be set ; ::_thesis: for v being Vertex of G holds ( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ) let v be Vertex of G; ::_thesis: ( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ) hereby ::_thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies e in v .edgesInOut() ) assume A1: e in v .edgesInOut() ; ::_thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) hence e in the_Edges_of G ; ::_thesis: ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ( e in v .edgesIn() or e in v .edgesOut() ) by A1, XBOOLE_0:def_3; hence ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by Lm8, Lm9; ::_thesis: verum end; assume ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ; ::_thesis: e in v .edgesInOut() then ( e in v .edgesIn() or e in v .edgesOut() ) by Lm8, Lm9; hence e in v .edgesInOut() by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th62: :: GLIB_000:62 for G being _Graph for e, x being set for v1 being Vertex of G st e Joins v1,x,G holds e in v1 .edgesInOut() proof let G be _Graph; ::_thesis: for e, x being set for v1 being Vertex of G st e Joins v1,x,G holds e in v1 .edgesInOut() let e, x be set ; ::_thesis: for v1 being Vertex of G st e Joins v1,x,G holds e in v1 .edgesInOut() let v1 be Vertex of G; ::_thesis: ( e Joins v1,x,G implies e in v1 .edgesInOut() ) assume A1: e Joins v1,x,G ; ::_thesis: e in v1 .edgesInOut() then A2: ( ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = x ) or ( (the_Source_of G) . e = x & (the_Target_of G) . e = v1 ) ) by Def13; e in the_Edges_of G by A1, Def13; hence e in v1 .edgesInOut() by A2, Th61; ::_thesis: verum end; theorem Th63: :: GLIB_000:63 for G being _Graph for e being set for v1, v2 being Vertex of G holds ( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) proof let G be _Graph; ::_thesis: for e being set for v1, v2 being Vertex of G holds ( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) let e be set ; ::_thesis: for v1, v2 being Vertex of G holds ( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) let v1, v2 be Vertex of G; ::_thesis: ( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) assume A1: e Joins v1,v2,G ; ::_thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) then A2: e in the_Edges_of G by Def13; now__::_thesis:_(_(_e_in_v1_.edgesIn()_&_e_in_v2_.edgesOut()_)_or_(_e_in_v2_.edgesIn()_&_e_in_v1_.edgesOut()_)_) percases ( ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) or ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ) by A1, Def13; suppose ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ; ::_thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A2, Lm8, Lm9; ::_thesis: verum end; suppose ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ; ::_thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A2, Lm8, Lm9; ::_thesis: verum end; end; end; hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) ; ::_thesis: verum end; theorem :: GLIB_000:64 for G being _Graph for e being set for v1 being Vertex of G holds ( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G ) proof let G be _Graph; ::_thesis: for e being set for v1 being Vertex of G holds ( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G ) let e be set ; ::_thesis: for v1 being Vertex of G holds ( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G ) let v1 be Vertex of G; ::_thesis: ( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G ) hereby ::_thesis: ( ex v2 being Vertex of G st e Joins v1,v2,G implies e in v1 .edgesInOut() ) assume A1: e in v1 .edgesInOut() ; ::_thesis: ex v2 being Vertex of G st e Joins v1,v2,G now__::_thesis:_ex_v2_being_Vertex_of_G_st_e_Joins_v1,v2,G percases ( (the_Source_of G) . e = v1 or (the_Target_of G) . e = v1 ) by A1, Th61; supposeA2: (the_Source_of G) . e = v1 ; ::_thesis: ex v2 being Vertex of G st e Joins v1,v2,G set v2 = (the_Target_of G) . e; reconsider v2 = (the_Target_of G) . e as Vertex of G by A1, FUNCT_2:5; take v2 = v2; ::_thesis: e Joins v1,v2,G thus e Joins v1,v2,G by A1, A2, Def13; ::_thesis: verum end; supposeA3: (the_Target_of G) . e = v1 ; ::_thesis: ex v2 being Vertex of G st e Joins v1,v2,G set v2 = (the_Source_of G) . e; reconsider v2 = (the_Source_of G) . e as Vertex of G by A1, FUNCT_2:5; take v2 = v2; ::_thesis: e Joins v1,v2,G thus e Joins v1,v2,G by A1, A3, Def13; ::_thesis: verum end; end; end; hence ex v2 being Vertex of G st e Joins v1,v2,G ; ::_thesis: verum end; given v2 being Vertex of G such that A4: e Joins v1,v2,G ; ::_thesis: e in v1 .edgesInOut() thus e in v1 .edgesInOut() by A4, Th62; ::_thesis: verum end; theorem :: GLIB_000:65 for G being _Graph for e, x, y being set for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds v = y proof let G be _Graph; ::_thesis: for e, x, y being set for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds v = y let e, x, y be set ; ::_thesis: for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds v = y let v be Vertex of G; ::_thesis: ( e in v .edgesInOut() & e Joins x,y,G & not v = x implies v = y ) assume that A1: e in v .edgesInOut() and A2: e Joins x,y,G ; ::_thesis: ( v = x or v = y ) now__::_thesis:_(_v_<>_x_implies_v_=_y_) assume A3: v <> x ; ::_thesis: v = y now__::_thesis:_v_=_y percases ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by A1, Th61; suppose (the_Source_of G) . e = v ; ::_thesis: v = y hence v = y by A2, A3, Def13; ::_thesis: verum end; suppose (the_Target_of G) . e = v ; ::_thesis: v = y hence v = y by A2, A3, Def13; ::_thesis: verum end; end; end; hence v = y ; ::_thesis: verum end; hence ( v = x or v = y ) ; ::_thesis: verum end; theorem :: GLIB_000:66 for G being _Graph for e being set for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( v1 .adj e = v2 & v2 .adj e = v1 ) proof let G be _Graph; ::_thesis: for e being set for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( v1 .adj e = v2 & v2 .adj e = v1 ) let e be set ; ::_thesis: for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( v1 .adj e = v2 & v2 .adj e = v1 ) let v1, v2 be Vertex of G; ::_thesis: ( e Joins v1,v2,G implies ( v1 .adj e = v2 & v2 .adj e = v1 ) ) assume A1: e Joins v1,v2,G ; ::_thesis: ( v1 .adj e = v2 & v2 .adj e = v1 ) then A2: e in v1 .edgesInOut() by Th62; now__::_thesis:_(_v1_.adj_e_=_v2_&_v2_.adj_e_=_v1_) percases ( ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) or ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ) by A1, Def13; supposeA3: ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ; ::_thesis: ( v1 .adj e = v2 & v2 .adj e = v1 ) hence v1 .adj e = v2 by A2, Def41; ::_thesis: v2 .adj e = v1 now__::_thesis:_v2_.adj_e_=_v1 percases ( v1 = v2 or v1 <> v2 ) ; suppose v1 = v2 ; ::_thesis: v2 .adj e = v1 hence v2 .adj e = v1 by A2, A3, Def41; ::_thesis: verum end; suppose v1 <> v2 ; ::_thesis: v2 .adj e = v1 hence v2 .adj e = v1 by A2, A3, Def41; ::_thesis: verum end; end; end; hence v2 .adj e = v1 ; ::_thesis: verum end; supposeA4: ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ; ::_thesis: ( v1 .adj e = v2 & v2 .adj e = v1 ) now__::_thesis:_v1_.adj_e_=_v2 percases ( v1 = v2 or v1 <> v2 ) ; suppose v1 = v2 ; ::_thesis: v1 .adj e = v2 hence v1 .adj e = v2 by A2, A4, Def41; ::_thesis: verum end; suppose v1 <> v2 ; ::_thesis: v1 .adj e = v2 hence v1 .adj e = v2 by A2, A4, Def41; ::_thesis: verum end; end; end; hence v1 .adj e = v2 ; ::_thesis: v2 .adj e = v1 thus v2 .adj e = v1 by A2, A4, Def41; ::_thesis: verum end; end; end; hence ( v1 .adj e = v2 & v2 .adj e = v1 ) ; ::_thesis: verum end; theorem :: GLIB_000:67 for G being _Graph for e being set for v being Vertex of G holds ( e in v .edgesInOut() iff e Joins v,v .adj e,G ) proof let G be _Graph; ::_thesis: for e being set for v being Vertex of G holds ( e in v .edgesInOut() iff e Joins v,v .adj e,G ) let e be set ; ::_thesis: for v being Vertex of G holds ( e in v .edgesInOut() iff e Joins v,v .adj e,G ) let v be Vertex of G; ::_thesis: ( e in v .edgesInOut() iff e Joins v,v .adj e,G ) hereby ::_thesis: ( e Joins v,v .adj e,G implies e in v .edgesInOut() ) assume A1: e in v .edgesInOut() ; ::_thesis: e Joins v,v .adj e,G then A2: ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by Th61; now__::_thesis:_e_Joins_v,v_.adj_e,G percases ( (the_Target_of G) . e = v or (the_Target_of G) . e <> v ) ; supposeA3: (the_Target_of G) . e = v ; ::_thesis: e Joins v,v .adj e,G then v .adj e = (the_Source_of G) . e by A1, Def41; hence e Joins v,v .adj e,G by A1, A3, Def13; ::_thesis: verum end; supposeA4: (the_Target_of G) . e <> v ; ::_thesis: e Joins v,v .adj e,G then v .adj e = (the_Target_of G) . e by A1, A2, Def41; hence e Joins v,v .adj e,G by A1, A2, A4, Def13; ::_thesis: verum end; end; end; hence e Joins v,v .adj e,G ; ::_thesis: verum end; assume e Joins v,v .adj e,G ; ::_thesis: e in v .edgesInOut() hence e in v .edgesInOut() by Th62; ::_thesis: verum end; theorem :: GLIB_000:68 for G being finite _Graph for e being set for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( 1 <= v1 .degree() & 1 <= v2 .degree() ) proof let G be finite _Graph; ::_thesis: for e being set for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( 1 <= v1 .degree() & 1 <= v2 .degree() ) let e be set ; ::_thesis: for v1, v2 being Vertex of G st e Joins v1,v2,G holds ( 1 <= v1 .degree() & 1 <= v2 .degree() ) let v1, v2 be Vertex of G; ::_thesis: ( e Joins v1,v2,G implies ( 1 <= v1 .degree() & 1 <= v2 .degree() ) ) assume A1: e Joins v1,v2,G ; ::_thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() ) now__::_thesis:_(_1_<=_v1_.degree()_&_1_<=_v2_.degree()_) percases ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A1, Th63; supposeA2: ( e in v1 .edgesIn() & e in v2 .edgesOut() ) ; ::_thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() ) then for x being set st x in {e} holds x in v1 .edgesIn() by TARSKI:def_1; then {e} c= v1 .edgesIn() by TARSKI:def_3; then card {e} <= card (v1 .edgesIn()) by NAT_1:43; then 1 <= v1 .inDegree() by CARD_1:30; hence 1 <= v1 .degree() by NAT_1:12; ::_thesis: 1 <= v2 .degree() for x being set st x in {e} holds x in v2 .edgesOut() by A2, TARSKI:def_1; then {e} c= v2 .edgesOut() by TARSKI:def_3; then card {e} <= card (v2 .edgesOut()) by NAT_1:43; then 1 <= v2 .outDegree() by CARD_1:30; hence 1 <= v2 .degree() by NAT_1:12; ::_thesis: verum end; supposeA3: ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ; ::_thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() ) then for x being set st x in {e} holds x in v1 .edgesOut() by TARSKI:def_1; then {e} c= v1 .edgesOut() by TARSKI:def_3; then card {e} <= card (v1 .edgesOut()) by NAT_1:43; then 1 <= v1 .outDegree() by CARD_1:30; hence 1 <= v1 .degree() by NAT_1:12; ::_thesis: 1 <= v2 .degree() for x being set st x in {e} holds x in v2 .edgesIn() by A3, TARSKI:def_1; then {e} c= v2 .edgesIn() by TARSKI:def_3; then card {e} <= card (v2 .edgesIn()) by NAT_1:43; then 1 <= v2 .inDegree() by CARD_1:30; hence 1 <= v2 .degree() by NAT_1:12; ::_thesis: verum end; end; end; hence ( 1 <= v1 .degree() & 1 <= v2 .degree() ) ; ::_thesis: verum end; theorem Th69: :: GLIB_000:69 for G being _Graph for x being set for v being Vertex of G holds ( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G ) proof let G be _Graph; ::_thesis: for x being set for v being Vertex of G holds ( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G ) let x be set ; ::_thesis: for v being Vertex of G holds ( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G ) let v be Vertex of G; ::_thesis: ( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G ) hereby ::_thesis: ( ex e being set st e DJoins x,v,G implies x in v .inNeighbors() ) assume x in v .inNeighbors() ; ::_thesis: ex e being set st e DJoins x,v,G then consider e being set such that A1: e in dom (the_Source_of G) and A2: e in v .edgesIn() and A3: x = (the_Source_of G) . e by FUNCT_1:def_6; take e = e; ::_thesis: e DJoins x,v,G (the_Target_of G) . e = v by A2, Lm8; hence e DJoins x,v,G by A1, A3, Def14; ::_thesis: verum end; given e being set such that A4: e DJoins x,v,G ; ::_thesis: x in v .inNeighbors() A5: e in the_Edges_of G by A4, Def14; then A6: e in dom (the_Source_of G) by FUNCT_2:def_1; (the_Target_of G) . e = v by A4, Def14; then A7: e in v .edgesIn() by A5, Lm8; (the_Source_of G) . e = x by A4, Def14; hence x in v .inNeighbors() by A7, A6, FUNCT_1:def_6; ::_thesis: verum end; theorem Th70: :: GLIB_000:70 for G being _Graph for x being set for v being Vertex of G holds ( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G ) proof let G be _Graph; ::_thesis: for x being set for v being Vertex of G holds ( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G ) let x be set ; ::_thesis: for v being Vertex of G holds ( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G ) let v be Vertex of G; ::_thesis: ( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G ) hereby ::_thesis: ( ex e being set st e DJoins v,x,G implies x in v .outNeighbors() ) assume x in v .outNeighbors() ; ::_thesis: ex e being set st e DJoins v,x,G then consider e being set such that A1: e in dom (the_Target_of G) and A2: e in v .edgesOut() and A3: x = (the_Target_of G) . e by FUNCT_1:def_6; take e = e; ::_thesis: e DJoins v,x,G (the_Source_of G) . e = v by A2, Lm9; hence e DJoins v,x,G by A1, A3, Def14; ::_thesis: verum end; given e being set such that A4: e DJoins v,x,G ; ::_thesis: x in v .outNeighbors() A5: e in the_Edges_of G by A4, Def14; then A6: e in dom (the_Target_of G) by FUNCT_2:def_1; (the_Source_of G) . e = v by A4, Def14; then A7: e in v .edgesOut() by A5, Lm9; (the_Target_of G) . e = x by A4, Def14; hence x in v .outNeighbors() by A7, A6, FUNCT_1:def_6; ::_thesis: verum end; theorem Th71: :: GLIB_000:71 for G being _Graph for x being set for v being Vertex of G holds ( x in v .allNeighbors() iff ex e being set st e Joins v,x,G ) proof let G be _Graph; ::_thesis: for x being set for v being Vertex of G holds ( x in v .allNeighbors() iff ex e being set st e Joins v,x,G ) let x be set ; ::_thesis: for v being Vertex of G holds ( x in v .allNeighbors() iff ex e being set st e Joins v,x,G ) let v be Vertex of G; ::_thesis: ( x in v .allNeighbors() iff ex e being set st e Joins v,x,G ) hereby ::_thesis: ( ex e being set st e Joins v,x,G implies x in v .allNeighbors() ) assume A1: x in v .allNeighbors() ; ::_thesis: ex e being set st e Joins v,x,G now__::_thesis:_ex_e_being_set_st_e_Joins_v,x,G percases ( x in v .inNeighbors() or x in v .outNeighbors() ) by A1, XBOOLE_0:def_3; suppose x in v .inNeighbors() ; ::_thesis: ex e being set st e Joins v,x,G then consider e being set such that A2: e DJoins x,v,G by Th69; take e = e; ::_thesis: e Joins v,x,G thus e Joins v,x,G by A2, Lm2; ::_thesis: verum end; suppose x in v .outNeighbors() ; ::_thesis: ex e being set st e Joins v,x,G then consider e being set such that A3: e DJoins v,x,G by Th70; take e = e; ::_thesis: e Joins v,x,G thus e Joins v,x,G by A3, Lm2; ::_thesis: verum end; end; end; hence ex e being set st e Joins v,x,G ; ::_thesis: verum end; assume ex e being set st e Joins v,x,G ; ::_thesis: x in v .allNeighbors() then consider e being set such that A4: e Joins v,x,G ; now__::_thesis:_x_in_(v_.inNeighbors())_\/_(v_.outNeighbors()) percases ( e DJoins x,v,G or e DJoins v,x,G ) by A4, Lm2; suppose e DJoins x,v,G ; ::_thesis: x in (v .inNeighbors()) \/ (v .outNeighbors()) then x in v .inNeighbors() by Th69; hence x in (v .inNeighbors()) \/ (v .outNeighbors()) by XBOOLE_0:def_3; ::_thesis: verum end; suppose e DJoins v,x,G ; ::_thesis: x in (v .inNeighbors()) \/ (v .outNeighbors()) then x in v .outNeighbors() by Th70; hence x in (v .inNeighbors()) \/ (v .outNeighbors()) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in v .allNeighbors() ; ::_thesis: verum end; theorem Th72: :: GLIB_000:72 for G1 being _Graph for G2 being Subgraph of G1 for x, y, e being set holds ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for x, y, e being set holds ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) let G2 be Subgraph of G1; ::_thesis: for x, y, e being set holds ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) let x, y, e be set ; ::_thesis: ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) thus ( e Joins x,y,G2 implies e Joins x,y,G1 ) by Lm5; ::_thesis: ( ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) hereby ::_thesis: ( ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) ) assume A1: e DJoins x,y,G2 ; ::_thesis: e DJoins x,y,G1 then A2: e in the_Edges_of G2 by Def14; (the_Target_of G2) . e = y by A1, Def14; then A3: (the_Target_of G1) . e = y by A2, Def32; (the_Source_of G2) . e = x by A1, Def14; then (the_Source_of G1) . e = x by A2, Def32; hence e DJoins x,y,G1 by A2, A3, Def14; ::_thesis: verum end; hereby ::_thesis: ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) assume A4: e SJoins x,y,G2 ; ::_thesis: e SJoins x,y,G1 then A5: ( ( (the_Source_of G2) . e in x & (the_Target_of G2) . e in y ) or ( (the_Source_of G2) . e in y & (the_Target_of G2) . e in x ) ) by Def15; A6: e in the_Edges_of G2 by A4, Def15; then ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by Def32; hence e SJoins x,y,G1 by A6, A5, Def15; ::_thesis: verum end; assume A7: e DSJoins x,y,G2 ; ::_thesis: e DSJoins x,y,G1 then A8: ( (the_Source_of G2) . e in x & (the_Target_of G2) . e in y ) by Def16; A9: e in the_Edges_of G2 by A7, Def16; then ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by Def32; hence e DSJoins x,y,G1 by A9, A8, Def16; ::_thesis: verum end; theorem :: GLIB_000:73 for G1 being _Graph for G2 being Subgraph of G1 for x, y, e being set st e in the_Edges_of G2 holds ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for x, y, e being set st e in the_Edges_of G2 holds ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) let G2 be Subgraph of G1; ::_thesis: for x, y, e being set st e in the_Edges_of G2 holds ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) let x, y, e be set ; ::_thesis: ( e in the_Edges_of G2 implies ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) ) assume A1: e in the_Edges_of G2 ; ::_thesis: ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) hereby ::_thesis: ( ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) assume e Joins x,y,G1 ; ::_thesis: e Joins x,y,G2 then A2: ( ( (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) or ( (the_Source_of G1) . e = y & (the_Target_of G1) . e = x ) ) by Def13; ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by A1, Def32; hence e Joins x,y,G2 by A1, A2, Def13; ::_thesis: verum end; (the_Target_of G2) . e = ((the_Target_of G1) | (the_Edges_of G2)) . e by Th45; then A3: (the_Target_of G2) . e = (the_Target_of G1) . e by A1, FUNCT_1:49; hereby ::_thesis: ( ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) assume A4: e DJoins x,y,G1 ; ::_thesis: e DJoins x,y,G2 then (the_Target_of G1) . e = y by Def14; then A5: (the_Target_of G2) . e = y by A1, Def32; (the_Source_of G1) . e = x by A4, Def14; then (the_Source_of G2) . e = x by A1, Def32; hence e DJoins x,y,G2 by A1, A5, Def14; ::_thesis: verum end; hereby ::_thesis: ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) (the_Target_of G2) . e = ((the_Target_of G1) | (the_Edges_of G2)) . e by Th45; then A6: (the_Target_of G2) . e = (the_Target_of G1) . e by A1, FUNCT_1:49; assume e SJoins x,y,G1 ; ::_thesis: e SJoins x,y,G2 then A7: ( ( (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) or ( (the_Source_of G1) . e in y & (the_Target_of G1) . e in x ) ) by Def15; (the_Source_of G2) . e = ((the_Source_of G1) | (the_Edges_of G2)) . e by Th45; then (the_Source_of G2) . e = (the_Source_of G1) . e by A1, FUNCT_1:49; hence e SJoins x,y,G2 by A1, A7, A6, Def15; ::_thesis: verum end; assume e DSJoins x,y,G1 ; ::_thesis: e DSJoins x,y,G2 then A8: ( (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) by Def16; (the_Source_of G2) . e = ((the_Source_of G1) | (the_Edges_of G2)) . e by Th45; then (the_Source_of G2) . e = (the_Source_of G1) . e by A1, FUNCT_1:49; hence e DSJoins x,y,G2 by A1, A8, A3, Def16; ::_thesis: verum end; theorem :: GLIB_000:74 for G1 being _Graph for G2 being spanning Subgraph of G1 for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1 proof let G1 be _Graph; ::_thesis: for G2 being spanning Subgraph of G1 for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1 let G2 be spanning Subgraph of G1; ::_thesis: for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1 let G3 be spanning Subgraph of G2; ::_thesis: G3 is spanning Subgraph of G1 the_Vertices_of G3 = the_Vertices_of G2 by Def33 .= the_Vertices_of G1 by Def33 ; hence G3 is spanning Subgraph of G1 by Def33, Th43; ::_thesis: verum end; theorem :: GLIB_000:75 for G1 being finite _Graph for G2 being Subgraph of G1 holds ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() ) proof let G1 be finite _Graph; ::_thesis: for G2 being Subgraph of G1 holds ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() ) let G2 be Subgraph of G1; ::_thesis: ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() ) card (the_Vertices_of G2) <= card (the_Vertices_of G1) by NAT_1:43; hence G2 .order() <= G1 .order() ; ::_thesis: G2 .size() <= G1 .size() card (the_Edges_of G2) <= card (the_Edges_of G1) by NAT_1:43; hence G2 .size() <= G1 .size() ; ::_thesis: verum end; theorem :: GLIB_000:76 for G1 being _Graph for G2 being Subgraph of G1 for X being set holds ( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for X being set holds ( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) let G2 be Subgraph of G1; ::_thesis: for X being set holds ( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) let X be set ; ::_thesis: ( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) now__::_thesis:_for_e_being_set_st_e_in_G2_.edgesInto_X_holds_ e_in_G1_.edgesInto_X let e be set ; ::_thesis: ( e in G2 .edgesInto X implies e in G1 .edgesInto X ) assume A1: e in G2 .edgesInto X ; ::_thesis: e in G1 .edgesInto X then A2: (the_Target_of G2) . e = (the_Target_of G1) . e by Def32; ( e in the_Edges_of G2 & (the_Target_of G2) . e in X ) by A1, Def26; hence e in G1 .edgesInto X by A2, Def26; ::_thesis: verum end; hence A3: G2 .edgesInto X c= G1 .edgesInto X by TARSKI:def_3; ::_thesis: ( G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) then A4: G2 .edgesInto X c= G1 .edgesInOut X by XBOOLE_1:10; now__::_thesis:_for_e_being_set_st_e_in_G2_.edgesOutOf_X_holds_ e_in_G1_.edgesOutOf_X let e be set ; ::_thesis: ( e in G2 .edgesOutOf X implies e in G1 .edgesOutOf X ) assume A5: e in G2 .edgesOutOf X ; ::_thesis: e in G1 .edgesOutOf X then A6: (the_Source_of G2) . e = (the_Source_of G1) . e by Def32; ( e in the_Edges_of G2 & (the_Source_of G2) . e in X ) by A5, Def27; hence e in G1 .edgesOutOf X by A6, Def27; ::_thesis: verum end; hence A7: G2 .edgesOutOf X c= G1 .edgesOutOf X by TARSKI:def_3; ::_thesis: ( G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X ) then G2 .edgesOutOf X c= G1 .edgesInOut X by XBOOLE_1:10; hence G2 .edgesInOut X c= G1 .edgesInOut X by A4, XBOOLE_1:8; ::_thesis: G2 .edgesBetween X c= G1 .edgesBetween X thus G2 .edgesBetween X c= G1 .edgesBetween X by A3, A7, XBOOLE_1:27; ::_thesis: verum end; theorem :: GLIB_000:77 for G1 being _Graph for G2 being Subgraph of G1 for X, Y being set holds ( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for X, Y being set holds ( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) ) let G2 be Subgraph of G1; ::_thesis: for X, Y being set holds ( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) ) let X, Y be set ; ::_thesis: ( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) ) now__::_thesis:_for_x_being_set_st_x_in_G2_.edgesBetween_(X,Y)_holds_ x_in_G1_.edgesBetween_(X,Y) let x be set ; ::_thesis: ( x in G2 .edgesBetween (X,Y) implies x in G1 .edgesBetween (X,Y) ) assume x in G2 .edgesBetween (X,Y) ; ::_thesis: x in G1 .edgesBetween (X,Y) then x SJoins X,Y,G2 by Def30; then x SJoins X,Y,G1 by Th72; hence x in G1 .edgesBetween (X,Y) by Def30; ::_thesis: verum end; hence G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) by TARSKI:def_3; ::_thesis: G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) now__::_thesis:_for_x_being_set_st_x_in_G2_.edgesDBetween_(X,Y)_holds_ x_in_G1_.edgesDBetween_(X,Y) let x be set ; ::_thesis: ( x in G2 .edgesDBetween (X,Y) implies x in G1 .edgesDBetween (X,Y) ) assume x in G2 .edgesDBetween (X,Y) ; ::_thesis: x in G1 .edgesDBetween (X,Y) then x DSJoins X,Y,G2 by Def31; then x DSJoins X,Y,G1 by Th72; hence x in G1 .edgesDBetween (X,Y) by Def31; ::_thesis: verum end; hence G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) by TARSKI:def_3; ::_thesis: verum end; theorem Th78: :: GLIB_000:78 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) ) assume A1: v1 = v2 ; ::_thesis: ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) now__::_thesis:_for_x_being_set_st_x_in_v2_.edgesIn()_holds_ x_in_v1_.edgesIn() let x be set ; ::_thesis: ( x in v2 .edgesIn() implies x in v1 .edgesIn() ) assume A2: x in v2 .edgesIn() ; ::_thesis: x in v1 .edgesIn() then (the_Target_of G2) . x = v2 by Lm8; then A3: (the_Target_of G1) . x = v1 by A1, A2, Def32; x in the_Edges_of G2 by A2; hence x in v1 .edgesIn() by A3, Lm8; ::_thesis: verum end; hence v2 .edgesIn() c= v1 .edgesIn() by TARSKI:def_3; ::_thesis: ( v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() ) now__::_thesis:_for_x_being_set_st_x_in_v2_.edgesOut()_holds_ x_in_v1_.edgesOut() let x be set ; ::_thesis: ( x in v2 .edgesOut() implies x in v1 .edgesOut() ) assume A4: x in v2 .edgesOut() ; ::_thesis: x in v1 .edgesOut() then (the_Source_of G2) . x = v2 by Lm9; then A5: (the_Source_of G1) . x = v1 by A1, A4, Def32; x in the_Edges_of G2 by A4; hence x in v1 .edgesOut() by A5, Lm9; ::_thesis: verum end; hence v2 .edgesOut() c= v1 .edgesOut() by TARSKI:def_3; ::_thesis: v2 .edgesInOut() c= v1 .edgesInOut() now__::_thesis:_for_x_being_set_st_x_in_v2_.edgesInOut()_holds_ x_in_v1_.edgesInOut() let x be set ; ::_thesis: ( x in v2 .edgesInOut() implies x in v1 .edgesInOut() ) assume A6: x in v2 .edgesInOut() ; ::_thesis: x in v1 .edgesInOut() then ( (the_Source_of G2) . x = v2 or (the_Target_of G2) . x = v2 ) by Th61; then A7: ( (the_Source_of G1) . x = v1 or (the_Target_of G1) . x = v1 ) by A1, A6, Def32; x in the_Edges_of G2 by A6; hence x in v1 .edgesInOut() by A7, Th61; ::_thesis: verum end; hence v2 .edgesInOut() c= v1 .edgesInOut() by TARSKI:def_3; ::_thesis: verum end; theorem Th79: :: GLIB_000:79 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) ) assume A1: v1 = v2 ; ::_thesis: ( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_v2_.edgesIn()_implies_x_in_(v1_.edgesIn())_/\_(the_Edges_of_G2)_)_&_(_x_in_(v1_.edgesIn())_/\_(the_Edges_of_G2)_implies_x_in_v2_.edgesIn()_)_) let x be set ; ::_thesis: ( ( x in v2 .edgesIn() implies x in (v1 .edgesIn()) /\ (the_Edges_of G2) ) & ( x in (v1 .edgesIn()) /\ (the_Edges_of G2) implies x in v2 .edgesIn() ) ) hereby ::_thesis: ( x in (v1 .edgesIn()) /\ (the_Edges_of G2) implies x in v2 .edgesIn() ) assume A2: x in v2 .edgesIn() ; ::_thesis: x in (v1 .edgesIn()) /\ (the_Edges_of G2) v2 .edgesIn() c= v1 .edgesIn() by A1, Th78; hence x in (v1 .edgesIn()) /\ (the_Edges_of G2) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: x in (v1 .edgesIn()) /\ (the_Edges_of G2) ; ::_thesis: x in v2 .edgesIn() then A4: x in the_Edges_of G2 by XBOOLE_0:def_4; x in v1 .edgesIn() by A3, XBOOLE_0:def_4; then (the_Target_of G1) . x = v1 by Lm8; then (the_Target_of G2) . x = v2 by A1, A4, Def32; hence x in v2 .edgesIn() by A4, Lm8; ::_thesis: verum end; hence A5: v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) by TARSKI:1; ::_thesis: ( v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) ) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_v2_.edgesOut()_implies_x_in_(v1_.edgesOut())_/\_(the_Edges_of_G2)_)_&_(_x_in_(v1_.edgesOut())_/\_(the_Edges_of_G2)_implies_x_in_v2_.edgesOut()_)_) let x be set ; ::_thesis: ( ( x in v2 .edgesOut() implies x in (v1 .edgesOut()) /\ (the_Edges_of G2) ) & ( x in (v1 .edgesOut()) /\ (the_Edges_of G2) implies x in v2 .edgesOut() ) ) hereby ::_thesis: ( x in (v1 .edgesOut()) /\ (the_Edges_of G2) implies x in v2 .edgesOut() ) assume A6: x in v2 .edgesOut() ; ::_thesis: x in (v1 .edgesOut()) /\ (the_Edges_of G2) v2 .edgesOut() c= v1 .edgesOut() by A1, Th78; hence x in (v1 .edgesOut()) /\ (the_Edges_of G2) by A6, XBOOLE_0:def_4; ::_thesis: verum end; assume A7: x in (v1 .edgesOut()) /\ (the_Edges_of G2) ; ::_thesis: x in v2 .edgesOut() then A8: x in the_Edges_of G2 by XBOOLE_0:def_4; x in v1 .edgesOut() by A7, XBOOLE_0:def_4; then (the_Source_of G1) . x = v1 by Lm9; then (the_Source_of G2) . x = v2 by A1, A8, Def32; hence x in v2 .edgesOut() by A8, Lm9; ::_thesis: verum end; hence A9: v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) by TARSKI:1; ::_thesis: v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(v1_.edgesInOut())_/\_(the_Edges_of_G2)_implies_x_in_v2_.edgesInOut()_)_&_(_x_in_v2_.edgesInOut()_implies_x_in_(v1_.edgesInOut())_/\_(the_Edges_of_G2)_)_) let x be set ; ::_thesis: ( ( x in (v1 .edgesInOut()) /\ (the_Edges_of G2) implies x in v2 .edgesInOut() ) & ( x in v2 .edgesInOut() implies x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ) ) hereby ::_thesis: ( x in v2 .edgesInOut() implies x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ) assume A10: x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ; ::_thesis: x in v2 .edgesInOut() then A11: x in the_Edges_of G2 by XBOOLE_0:def_4; A12: x in v1 .edgesInOut() by A10, XBOOLE_0:def_4; now__::_thesis:_x_in_v2_.edgesInOut() percases ( x in v1 .edgesIn() or x in v1 .edgesOut() ) by A12, XBOOLE_0:def_3; suppose x in v1 .edgesIn() ; ::_thesis: x in v2 .edgesInOut() then x in (v1 .edgesIn()) /\ (the_Edges_of G2) by A11, XBOOLE_0:def_4; hence x in v2 .edgesInOut() by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose x in v1 .edgesOut() ; ::_thesis: x in v2 .edgesInOut() then x in (v1 .edgesOut()) /\ (the_Edges_of G2) by A11, XBOOLE_0:def_4; hence x in v2 .edgesInOut() by A9, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in v2 .edgesInOut() ; ::_thesis: verum end; assume A13: x in v2 .edgesInOut() ; ::_thesis: x in (v1 .edgesInOut()) /\ (the_Edges_of G2) now__::_thesis:_x_in_(v1_.edgesInOut())_/\_(the_Edges_of_G2) percases ( x in (v1 .edgesIn()) /\ (the_Edges_of G2) or x in (v1 .edgesOut()) /\ (the_Edges_of G2) ) by A5, A9, A13, XBOOLE_0:def_3; supposeA14: x in (v1 .edgesIn()) /\ (the_Edges_of G2) ; ::_thesis: x in (v1 .edgesInOut()) /\ (the_Edges_of G2) then x in v1 .edgesIn() by XBOOLE_0:def_4; then A15: x in (v1 .edgesIn()) \/ (v1 .edgesOut()) by XBOOLE_0:def_3; x in the_Edges_of G2 by A14, XBOOLE_0:def_4; hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) by A15, XBOOLE_0:def_4; ::_thesis: verum end; supposeA16: x in (v1 .edgesOut()) /\ (the_Edges_of G2) ; ::_thesis: x in (v1 .edgesInOut()) /\ (the_Edges_of G2) then x in v1 .edgesOut() by XBOOLE_0:def_4; then A17: x in (v1 .edgesIn()) \/ (v1 .edgesOut()) by XBOOLE_0:def_3; x in the_Edges_of G2 by A16, XBOOLE_0:def_4; hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) by A17, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ; ::_thesis: verum end; hence v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) by TARSKI:1; ::_thesis: verum end; theorem :: GLIB_000:80 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 for e being set st v1 = v2 & e in the_Edges_of G2 holds v1 .adj e = v2 .adj e proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 for e being set st v1 = v2 & e in the_Edges_of G2 holds v1 .adj e = v2 .adj e let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 for e being set st v1 = v2 & e in the_Edges_of G2 holds v1 .adj e = v2 .adj e let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 for e being set st v1 = v2 & e in the_Edges_of G2 holds v1 .adj e = v2 .adj e let v2 be Vertex of G2; ::_thesis: for e being set st v1 = v2 & e in the_Edges_of G2 holds v1 .adj e = v2 .adj e let e be set ; ::_thesis: ( v1 = v2 & e in the_Edges_of G2 implies v1 .adj e = v2 .adj e ) assume that A1: v1 = v2 and A2: e in the_Edges_of G2 ; ::_thesis: v1 .adj e = v2 .adj e A3: ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by A2, Def32; now__::_thesis:_v1_.adj_e_=_v2_.adj_e percases ( (the_Target_of G1) . e = v1 or ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e <> v1 ) or ( (the_Source_of G1) . e <> v1 & (the_Target_of G1) . e <> v1 ) ) ; supposeA4: (the_Target_of G1) . e = v1 ; ::_thesis: v1 .adj e = v2 .adj e hence v1 .adj e = (the_Source_of G1) . e by A2, Def41 .= v2 .adj e by A1, A2, A3, A4, Def41 ; ::_thesis: verum end; supposeA5: ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e <> v1 ) ; ::_thesis: v1 .adj e = v2 .adj e hence v1 .adj e = (the_Target_of G1) . e by A2, Def41 .= v2 .adj e by A1, A2, A3, A5, Def41 ; ::_thesis: verum end; supposeA6: ( (the_Source_of G1) . e <> v1 & (the_Target_of G1) . e <> v1 ) ; ::_thesis: v1 .adj e = v2 .adj e hence v1 .adj e = v2 by A1, Def41 .= v2 .adj e by A1, A3, A6, Def41 ; ::_thesis: verum end; end; end; hence v1 .adj e = v2 .adj e ; ::_thesis: verum end; theorem :: GLIB_000:81 for G1 being finite _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) proof let G1 be finite _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) ) assume A1: v1 = v2 ; ::_thesis: ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) then v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) by Th79; hence A2: v2 .inDegree() <= v1 .inDegree() by NAT_1:43, XBOOLE_1:17; ::_thesis: ( v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) A3: v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) by A1, Th79; hence v2 .outDegree() <= v1 .outDegree() by NAT_1:43, XBOOLE_1:17; ::_thesis: v2 .degree() <= v1 .degree() v2 .outDegree() <= card (v1 .edgesOut()) by A3, NAT_1:43, XBOOLE_1:17; hence v2 .degree() <= v1 .degree() by A2, XREAL_1:7; ::_thesis: verum end; theorem :: GLIB_000:82 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) ) assume A1: v1 = v2 ; ::_thesis: ( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) now__::_thesis:_for_v_being_set_st_v_in_v2_.inNeighbors()_holds_ v_in_v1_.inNeighbors() let v be set ; ::_thesis: ( v in v2 .inNeighbors() implies v in v1 .inNeighbors() ) assume v in v2 .inNeighbors() ; ::_thesis: v in v1 .inNeighbors() then consider e being set such that A2: e DJoins v,v2,G2 by Th69; e DJoins v,v1,G1 by A1, A2, Th72; hence v in v1 .inNeighbors() by Th69; ::_thesis: verum end; hence v2 .inNeighbors() c= v1 .inNeighbors() by TARSKI:def_3; ::_thesis: ( v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() ) now__::_thesis:_for_v_being_set_st_v_in_v2_.outNeighbors()_holds_ v_in_v1_.outNeighbors() let v be set ; ::_thesis: ( v in v2 .outNeighbors() implies v in v1 .outNeighbors() ) assume v in v2 .outNeighbors() ; ::_thesis: v in v1 .outNeighbors() then consider e being set such that A3: e DJoins v2,v,G2 by Th70; e DJoins v1,v,G1 by A1, A3, Th72; hence v in v1 .outNeighbors() by Th70; ::_thesis: verum end; hence v2 .outNeighbors() c= v1 .outNeighbors() by TARSKI:def_3; ::_thesis: v2 .allNeighbors() c= v1 .allNeighbors() now__::_thesis:_for_v_being_set_st_v_in_v2_.allNeighbors()_holds_ v_in_v1_.allNeighbors() let v be set ; ::_thesis: ( v in v2 .allNeighbors() implies v in v1 .allNeighbors() ) assume v in v2 .allNeighbors() ; ::_thesis: v in v1 .allNeighbors() then consider e being set such that A4: e Joins v2,v,G2 by Th71; e Joins v1,v,G1 by A1, A4, Lm5; hence v in v1 .allNeighbors() by Th71; ::_thesis: verum end; hence v2 .allNeighbors() c= v1 .allNeighbors() by TARSKI:def_3; ::_thesis: verum end; theorem :: GLIB_000:83 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated let v2 be Vertex of G2; ::_thesis: ( v1 = v2 & v1 is isolated implies v2 is isolated ) assume ( v1 = v2 & v1 is isolated ) ; ::_thesis: v2 is isolated then ( v1 .edgesInOut() = {} & v2 .edgesInOut() c= v1 .edgesInOut() ) by Def49, Th78; then v2 .edgesInOut() = {} ; hence v2 is isolated by Def49; ::_thesis: verum end; theorem :: GLIB_000:84 for G1 being _Graph for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds v2 is isolated proof let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1 for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds v2 is isolated let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds v2 is isolated let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds v2 is isolated let v2 be Vertex of G2; ::_thesis: ( v1 = v2 & v1 is endvertex & not v2 is endvertex implies v2 is isolated ) assume that A1: v1 = v2 and A2: v1 is endvertex ; ::_thesis: ( v2 is endvertex or v2 is isolated ) consider e being set such that A3: v1 .edgesInOut() = {e} and A4: not e Joins v1,v1,G1 by A2, Def51; v2 .edgesInOut() c= v1 .edgesInOut() by A1, Th78; then A5: ( v2 .edgesInOut() = {} or v2 .edgesInOut() = {e} ) by A3, ZFMISC_1:33; now__::_thesis:_(_not_v2_is_isolated_implies_v2_is_endvertex_) assume A6: not v2 is isolated ; ::_thesis: v2 is endvertex not e Joins v2,v2,G2 by A1, A4, Lm5; hence v2 is endvertex by A5, A6, Def49, Def51; ::_thesis: verum end; hence ( v2 is endvertex or v2 is isolated ) ; ::_thesis: verum end; theorem Th85: :: GLIB_000:85 for G1, G2, G3 being _Graph st G1 == G2 & G2 == G3 holds G1 == G3 proof let G1, G2, G3 be _Graph; ::_thesis: ( G1 == G2 & G2 == G3 implies G1 == G3 ) assume that A1: G1 == G2 and A2: G2 == G3 ; ::_thesis: G1 == G3 A3: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1, Def34; A4: ( the_Source_of G2 = the_Source_of G3 & the_Target_of G2 = the_Target_of G3 ) by A2, Def34; A5: ( the_Vertices_of G2 = the_Vertices_of G3 & the_Edges_of G2 = the_Edges_of G3 ) by A2, Def34; ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A1, Def34; hence G1 == G3 by A3, A5, A4, Def34; ::_thesis: verum end; theorem Th86: :: GLIB_000:86 for G being _Graph for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds G1 == G2 proof let G be _Graph; ::_thesis: for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds G1 == G2 let G1, G2 be Subgraph of G; ::_thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 implies G1 == G2 ) assume that A1: the_Vertices_of G1 = the_Vertices_of G2 and A2: the_Edges_of G1 = the_Edges_of G2 ; ::_thesis: G1 == G2 A3: ( dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) = the_Edges_of G2 ) by FUNCT_2:def_1; now__::_thesis:_for_e_being_set_st_e_in_the_Edges_of_G1_holds_ (the_Target_of_G1)_._e_=_(the_Target_of_G2)_._e let e be set ; ::_thesis: ( e in the_Edges_of G1 implies (the_Target_of G1) . e = (the_Target_of G2) . e ) assume A4: e in the_Edges_of G1 ; ::_thesis: (the_Target_of G1) . e = (the_Target_of G2) . e then (the_Target_of G1) . e = (the_Target_of G) . e by Def32; hence (the_Target_of G1) . e = (the_Target_of G2) . e by A2, A4, Def32; ::_thesis: verum end; then A5: the_Target_of G1 = the_Target_of G2 by A2, A3, FUNCT_1:2; A6: now__::_thesis:_for_e_being_set_st_e_in_the_Edges_of_G1_holds_ (the_Source_of_G1)_._e_=_(the_Source_of_G2)_._e let e be set ; ::_thesis: ( e in the_Edges_of G1 implies (the_Source_of G1) . e = (the_Source_of G2) . e ) assume A7: e in the_Edges_of G1 ; ::_thesis: (the_Source_of G1) . e = (the_Source_of G2) . e then (the_Source_of G1) . e = (the_Source_of G) . e by Def32; hence (the_Source_of G1) . e = (the_Source_of G2) . e by A2, A7, Def32; ::_thesis: verum end; ( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G2 ) by FUNCT_2:def_1; then the_Source_of G1 = the_Source_of G2 by A2, A6, FUNCT_1:2; hence G1 == G2 by A1, A2, A5, Def34; ::_thesis: verum end; theorem Th87: :: GLIB_000:87 for G1, G2 being _Graph holds ( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) proof let G1, G2 be _Graph; ::_thesis: ( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) ( G1 is Subgraph of G2 & G2 is Subgraph of G1 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ) by Th41; hence ( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) by Def34; ::_thesis: verum end; theorem Th88: :: GLIB_000:88 for G1, G2 being _Graph for e, x, y, X, Y being set st G1 == G2 holds ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) proof let G1, G2 be _Graph; ::_thesis: for e, x, y, X, Y being set st G1 == G2 holds ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) let e, x, y, X, Y be set ; ::_thesis: ( G1 == G2 implies ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) ) assume G1 == G2 ; ::_thesis: ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) then G1 is Subgraph of G2 by Th87; hence ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) by Th72; ::_thesis: verum end; theorem :: GLIB_000:89 for G1, G2 being _Graph st G1 == G2 holds ( ( G1 is finite implies G2 is finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) proof let G1, G2 be _Graph; ::_thesis: ( G1 == G2 implies ( ( G1 is finite implies G2 is finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) ) assume A1: G1 == G2 ; ::_thesis: ( ( G1 is finite implies G2 is finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) then A2: the_Edges_of G1 = the_Edges_of G2 by Def34; A3: the_Vertices_of G1 = the_Vertices_of G2 by A1, Def34; hence ( G1 is finite implies G2 is finite ) by A2, Def17; ::_thesis: ( ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) A4: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1, Def34; A5: now__::_thesis:_(_G1_is_loopless_implies_G2_is_loopless_) assume G1 is loopless ; ::_thesis: G2 is loopless then for e being set holds ( not e in the_Edges_of G2 or not (the_Source_of G2) . e = (the_Target_of G2) . e ) by A2, A4, Def18; hence G2 is loopless by Def18; ::_thesis: verum end; hence ( G1 is loopless implies G2 is loopless ) ; ::_thesis: ( ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) hereby ::_thesis: ( ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) assume G1 is trivial ; ::_thesis: G2 is trivial then card (the_Vertices_of G2) = 1 by A3, Def19; hence G2 is trivial by Def19; ::_thesis: verum end; A6: now__::_thesis:_(_G1_is_non-multi_implies_G2_is_non-multi_) assume A7: G1 is non-multi ; ::_thesis: G2 is non-multi now__::_thesis:_for_e1,_e2,_v1,_v2_being_set_st_e1_Joins_v1,v2,G2_&_e2_Joins_v1,v2,G2_holds_ e1_=_e2 let e1, e2, v1, v2 be set ; ::_thesis: ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 implies e1 = e2 ) assume ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 ) ; ::_thesis: e1 = e2 then ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by A1, Th88; hence e1 = e2 by A7, Def20; ::_thesis: verum end; hence G2 is non-multi by Def20; ::_thesis: verum end; hence ( G1 is non-multi implies G2 is non-multi ) ; ::_thesis: ( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) A8: now__::_thesis:_(_G1_is_non-Dmulti_implies_G2_is_non-Dmulti_) assume A9: G1 is non-Dmulti ; ::_thesis: G2 is non-Dmulti now__::_thesis:_for_e1,_e2,_v1,_v2_being_set_st_e1_DJoins_v1,v2,G2_&_e2_DJoins_v1,v2,G2_holds_ e1_=_e2 let e1, e2, v1, v2 be set ; ::_thesis: ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 implies e1 = e2 ) assume ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 ) ; ::_thesis: e1 = e2 then ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) by A1, Th88; hence e1 = e2 by A9, Def21; ::_thesis: verum end; hence G2 is non-Dmulti by Def21; ::_thesis: verum end; hence ( G1 is non-Dmulti implies G2 is non-Dmulti ) ; ::_thesis: ( ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) ) thus ( G1 is simple implies G2 is simple ) by A5, A6; ::_thesis: ( G1 is Dsimple implies G2 is Dsimple ) thus ( G1 is Dsimple implies G2 is Dsimple ) by A5, A8; ::_thesis: verum end; theorem Th90: :: GLIB_000:90 for G1, G2 being _Graph for X, Y being set st G1 == G2 holds ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) proof let G1, G2 be _Graph; ::_thesis: for X, Y being set st G1 == G2 holds ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) let X, Y be set ; ::_thesis: ( G1 == G2 implies ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) ) assume A1: G1 == G2 ; ::_thesis: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) hence G1 .order() = G2 .order() by Def34; ::_thesis: ( G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) thus G1 .size() = G2 .size() by A1, Def34; ::_thesis: ( G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) A2: the_Edges_of G1 = the_Edges_of G2 by A1, Def34; A3: the_Target_of G1 = the_Target_of G2 by A1, Def34; A4: now__::_thesis:_for_e_being_set_holds_ (_e_in_G1_.edgesInto_X_iff_e_in_G2_.edgesInto_X_) let e be set ; ::_thesis: ( e in G1 .edgesInto X iff e in G2 .edgesInto X ) ( e in G1 .edgesInto X iff ( e in the_Edges_of G2 & (the_Target_of G2) . e in X ) ) by A2, A3, Def26; hence ( e in G1 .edgesInto X iff e in G2 .edgesInto X ) by Def26; ::_thesis: verum end; hence A5: G1 .edgesInto X = G2 .edgesInto X by TARSKI:1; ::_thesis: ( G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) A6: the_Source_of G1 = the_Source_of G2 by A1, Def34; A7: now__::_thesis:_for_e_being_set_holds_ (_e_in_G1_.edgesOutOf_X_iff_e_in_G2_.edgesOutOf_X_) let e be set ; ::_thesis: ( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X ) ( e in G1 .edgesOutOf X iff ( e in the_Edges_of G2 & (the_Source_of G2) . e in X ) ) by A2, A6, Def27; hence ( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X ) by Def27; ::_thesis: verum end; hence A8: G1 .edgesOutOf X = G2 .edgesOutOf X by TARSKI:1; ::_thesis: ( G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) thus G1 .edgesInOut X = G2 .edgesInOut X by A5, A7, TARSKI:1; ::_thesis: ( G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) thus G1 .edgesBetween X = G2 .edgesBetween X by A4, A8, TARSKI:1; ::_thesis: G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) now__::_thesis:_for_e_being_set_holds_ (_e_in_G2_.edgesDBetween_(X,Y)_iff_e_in_G1_.edgesDBetween_(X,Y)_) let e be set ; ::_thesis: ( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) ) ( e in G1 .edgesDBetween (X,Y) iff e DSJoins X,Y,G1 ) by Def31; then ( e in G1 .edgesDBetween (X,Y) iff e DSJoins X,Y,G2 ) by A1, Th88; hence ( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) ) by Def31; ::_thesis: verum end; hence G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) by TARSKI:1; ::_thesis: verum end; theorem Th91: :: GLIB_000:91 for G1, G2, G3 being _Graph st G1 == G2 & G3 is Subgraph of G1 holds G3 is Subgraph of G2 proof let G1, G2, G3 be _Graph; ::_thesis: ( G1 == G2 & G3 is Subgraph of G1 implies G3 is Subgraph of G2 ) assume that A1: G1 == G2 and A2: G3 is Subgraph of G1 ; ::_thesis: G3 is Subgraph of G2 the_Vertices_of G3 c= the_Vertices_of G1 by A2, Def32; hence the_Vertices_of G3 c= the_Vertices_of G2 by A1, Def34; :: according to GLIB_000:def_32 ::_thesis: ( the_Edges_of G3 c= the_Edges_of G2 & ( for e being set st e in the_Edges_of G3 holds ( (the_Source_of G3) . e = (the_Source_of G2) . e & (the_Target_of G3) . e = (the_Target_of G2) . e ) ) ) the_Edges_of G3 c= the_Edges_of G1 by A2, Def32; hence the_Edges_of G3 c= the_Edges_of G2 by A1, Def34; ::_thesis: for e being set st e in the_Edges_of G3 holds ( (the_Source_of G3) . e = (the_Source_of G2) . e & (the_Target_of G3) . e = (the_Target_of G2) . e ) let e be set ; ::_thesis: ( e in the_Edges_of G3 implies ( (the_Source_of G3) . e = (the_Source_of G2) . e & (the_Target_of G3) . e = (the_Target_of G2) . e ) ) assume A3: e in the_Edges_of G3 ; ::_thesis: ( (the_Source_of G3) . e = (the_Source_of G2) . e & (the_Target_of G3) . e = (the_Target_of G2) . e ) hence (the_Source_of G3) . e = (the_Source_of G1) . e by A2, Def32 .= (the_Source_of G2) . e by A1, Def34 ; ::_thesis: (the_Target_of G3) . e = (the_Target_of G2) . e thus (the_Target_of G3) . e = (the_Target_of G1) . e by A2, A3, Def32 .= (the_Target_of G2) . e by A1, Def34 ; ::_thesis: verum end; theorem :: GLIB_000:92 for G1, G2, G3 being _Graph st G1 == G2 & G1 is Subgraph of G3 holds G2 is Subgraph of G3 proof let G1, G2, G3 be _Graph; ::_thesis: ( G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3 ) assume that A1: G1 == G2 and A2: G1 is Subgraph of G3 ; ::_thesis: G2 is Subgraph of G3 A3: the_Edges_of G1 = the_Edges_of G2 by A1, Def34; A4: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1, Def34; the_Vertices_of G1 = the_Vertices_of G2 by A1, Def34; hence ( the_Vertices_of G2 c= the_Vertices_of G3 & the_Edges_of G2 c= the_Edges_of G3 ) by A2, A3, Def32; :: according to GLIB_000:def_32 ::_thesis: for e being set st e in the_Edges_of G2 holds ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) let e be set ; ::_thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) ) assume e in the_Edges_of G2 ; ::_thesis: ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) hence ( (the_Source_of G2) . e = (the_Source_of G3) . e & (the_Target_of G2) . e = (the_Target_of G3) . e ) by A2, A3, A4, Def32; ::_thesis: verum end; theorem :: GLIB_000:93 for G being _Graph for V, E being set for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2 proof let G be _Graph; ::_thesis: for V, E being set for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2 let V, E be set ; ::_thesis: for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2 let G1, G2 be inducedSubgraph of G,V,E; ::_thesis: G1 == G2 now__::_thesis:_G1_==_G2 percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: G1 == G2 then A2: ( the_Edges_of G1 = E & the_Edges_of G2 = E ) by Def37; ( the_Vertices_of G1 = V & the_Vertices_of G2 = V ) by A1, Def37; hence G1 == G2 by A2, Th86; ::_thesis: verum end; suppose ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: G1 == G2 then ( G1 == G & G2 == G ) by Def37; hence G1 == G2 by Th85; ::_thesis: verum end; end; end; hence G1 == G2 ; ::_thesis: verum end; theorem :: GLIB_000:94 for G1 being _Graph for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2 proof let G1 be _Graph; ::_thesis: for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2 let G2 be inducedSubgraph of G1,(the_Vertices_of G1); ::_thesis: G1 == G2 A1: the_Vertices_of G1 c= the_Vertices_of G1 ; then the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G1) by Def37; then A2: the_Edges_of G2 = the_Edges_of G1 by Th34; then the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G1) by Th45; then the_Source_of G2 = (the_Source_of G1) | (dom (the_Source_of G1)) ; then A3: the_Source_of G2 = the_Source_of G1 ; the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G1) by A2, Th45; then the_Target_of G2 = (the_Target_of G1) | (dom (the_Target_of G1)) ; then A4: the_Target_of G2 = the_Target_of G1 ; the_Vertices_of G2 = the_Vertices_of G1 by A1, Def37; hence G1 == G2 by A2, A3, A4, Def34; ::_thesis: verum end; theorem :: GLIB_000:95 for G1, G2 being _Graph for V, E being set for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E proof let G1, G2 be _Graph; ::_thesis: for V, E being set for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E let V, E be set ; ::_thesis: for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E let G3 be inducedSubgraph of G1,V,E; ::_thesis: ( G1 == G2 implies G3 is inducedSubgraph of G2,V,E ) assume A1: G1 == G2 ; ::_thesis: G3 is inducedSubgraph of G2,V,E now__::_thesis:_G3_is_inducedSubgraph_of_G2,V,E percases ( ( V is non empty Subset of (the_Vertices_of G1) & E c= G1 .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G1) or not E c= G1 .edgesBetween V ) ; supposeA2: ( V is non empty Subset of (the_Vertices_of G1) & E c= G1 .edgesBetween V ) ; ::_thesis: G3 is inducedSubgraph of G2,V,E then A3: ( the_Vertices_of G3 = V & the_Edges_of G3 = E ) by Def37; A4: G3 is Subgraph of G2 by A1, Th91; ( V is non empty Subset of (the_Vertices_of G2) & E c= G2 .edgesBetween V ) by A1, A2, Def34, Th90; hence G3 is inducedSubgraph of G2,V,E by A3, A4, Def37; ::_thesis: verum end; supposeA5: ( not V is non empty Subset of (the_Vertices_of G1) or not E c= G1 .edgesBetween V ) ; ::_thesis: G3 is inducedSubgraph of G2,V,E then A6: ( not V is non empty Subset of (the_Vertices_of G2) or not E c= G2 .edgesBetween V ) by A1, Def34, Th90; G3 == G1 by A5, Def37; then A7: G3 == G2 by A1, Th85; then G3 is Subgraph of G2 by Th87; hence G3 is inducedSubgraph of G2,V,E by A6, A7, Def37; ::_thesis: verum end; end; end; hence G3 is inducedSubgraph of G2,V,E ; ::_thesis: verum end; theorem Th96: :: GLIB_000:96 for G1, G2 being _Graph for e being set for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) proof let G1, G2 be _Graph; ::_thesis: for e being set for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) let e be set ; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 & G1 == G2 implies ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) ) assume that A1: v1 = v2 and A2: G1 == G2 ; ::_thesis: ( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus A3: v1 .edgesIn() = v2 .edgesIn() by A1, A2, Th90; ::_thesis: ( v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus A4: v1 .edgesOut() = v2 .edgesOut() by A1, A2, Th90; ::_thesis: ( v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus v1 .edgesInOut() = v2 .edgesInOut() by A1, A2, Th90; ::_thesis: ( v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) now__::_thesis:_v1_.adj_e_=_v2_.adj_e percases ( ( e in the_Edges_of G1 & (the_Target_of G1) . e = v1 ) or ( e in the_Edges_of G1 & (the_Source_of G1) . e = v1 & not (the_Target_of G1) . e = v1 ) or ( ( not e in the_Edges_of G1 or not (the_Target_of G1) . e = v1 ) & ( not e in the_Edges_of G1 or not (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) ) ) ; supposeA5: ( e in the_Edges_of G1 & (the_Target_of G1) . e = v1 ) ; ::_thesis: v1 .adj e = v2 .adj e then A6: ( e in the_Edges_of G2 & (the_Target_of G2) . e = v2 ) by A1, A2, Def34; thus v1 .adj e = (the_Source_of G1) . e by A5, Def41 .= (the_Source_of G2) . e by A2, Def34 .= v2 .adj e by A6, Def41 ; ::_thesis: verum end; supposeA7: ( e in the_Edges_of G1 & (the_Source_of G1) . e = v1 & not (the_Target_of G1) . e = v1 ) ; ::_thesis: v1 .adj e = v2 .adj e then A8: not (the_Target_of G2) . e = v2 by A1, A2, Def34; A9: ( e in the_Edges_of G2 & (the_Source_of G2) . e = v2 ) by A1, A2, A7, Def34; thus v1 .adj e = (the_Target_of G1) . e by A7, Def41 .= (the_Target_of G2) . e by A2, Def34 .= v2 .adj e by A9, A8, Def41 ; ::_thesis: verum end; supposeA10: ( ( not e in the_Edges_of G1 or not (the_Target_of G1) . e = v1 ) & ( not e in the_Edges_of G1 or not (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) ) ; ::_thesis: v1 .adj e = v2 .adj e then A11: ( ( not e in the_Edges_of G2 or not (the_Target_of G2) . e = v2 ) & ( not e in the_Edges_of G2 or not (the_Source_of G2) . e = v2 or (the_Target_of G2) . e = v2 ) ) by A1, A2, Def34; thus v1 .adj e = v2 by A1, A10, Def41 .= v2 .adj e by A11, Def41 ; ::_thesis: verum end; end; end; hence v1 .adj e = v2 .adj e ; ::_thesis: ( v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus v1 .inDegree() = v2 .inDegree() by A1, A2, Th90; ::_thesis: ( v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus v1 .outDegree() = v2 .outDegree() by A1, A2, Th90; ::_thesis: ( v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) hence v1 .degree() = v2 .degree() by A1, A2, Th90; ::_thesis: ( v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus v1 .inNeighbors() = v2 .inNeighbors() by A2, A3, Def34; ::_thesis: ( v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() ) thus v1 .outNeighbors() = v2 .outNeighbors() by A2, A4, Def34; ::_thesis: v1 .allNeighbors() = v2 .allNeighbors() hence v1 .allNeighbors() = v2 .allNeighbors() by A2, A3, Def34; ::_thesis: verum end; theorem :: GLIB_000:97 for G1, G2 being _Graph for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) proof let G1, G2 be _Graph; ::_thesis: for v1 being Vertex of G1 for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) let v2 be Vertex of G2; ::_thesis: ( v1 = v2 & G1 == G2 implies ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) ) assume A1: ( v1 = v2 & G1 == G2 ) ; ::_thesis: ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) hereby ::_thesis: ( v1 is endvertex implies v2 is endvertex ) assume v1 is isolated ; ::_thesis: v2 is isolated then v1 .edgesInOut() = {} by Def49; then v2 .edgesInOut() = {} by A1, Th96; hence v2 is isolated by Def49; ::_thesis: verum end; assume v1 is endvertex ; ::_thesis: v2 is endvertex then consider e being set such that A2: ( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 ) by Def51; ( v2 .edgesInOut() = {e} & not e Joins v2,v2,G2 ) by A1, A2, Th88, Th96; hence v2 is endvertex by Def51; ::_thesis: verum end; theorem Th98: :: GLIB_000:98 for G being _Graph for G1, G2 being Subgraph of G holds ( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) proof let G be _Graph; ::_thesis: for G1, G2 being Subgraph of G holds ( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) let G1, G2 be Subgraph of G; ::_thesis: ( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) assume A1: G1 c< G2 ; ::_thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) then G1 c= G2 by Def36; then A2: G1 is Subgraph of G2 by Def35; then A3: the_Vertices_of G1 c= the_Vertices_of G2 by Def32; A4: the_Edges_of G1 c= the_Edges_of G2 by A2, Def32; A5: not G1 == G2 by A1, Def36; now__::_thesis:_(_the_Vertices_of_G1_c<_the_Vertices_of_G2_or_the_Edges_of_G1_c<_the_Edges_of_G2_) percases ( the_Vertices_of G1 <> the_Vertices_of G2 or the_Edges_of G1 <> the_Edges_of G2 ) by A5, Th86; suppose the_Vertices_of G1 <> the_Vertices_of G2 ; ::_thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by A3, XBOOLE_0:def_8; ::_thesis: verum end; suppose the_Edges_of G1 <> the_Edges_of G2 ; ::_thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by A4, XBOOLE_0:def_8; ::_thesis: verum end; end; end; hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) ; ::_thesis: verum end; theorem :: GLIB_000:99 for G being _Graph for G1, G2 being Subgraph of G holds ( not G1 c< G2 or ex v being set st ( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st ( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) proof let G be _Graph; ::_thesis: for G1, G2 being Subgraph of G holds ( not G1 c< G2 or ex v being set st ( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st ( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) let G1, G2 be Subgraph of G; ::_thesis: ( not G1 c< G2 or ex v being set st ( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st ( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) assume G1 c< G2 ; ::_thesis: ( ex v being set st ( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st ( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) then ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by Th98; hence ( ex v being set st ( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st ( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) by XBOOLE_0:6; ::_thesis: verum end;