environ
vocabularies HIDDEN, NUMBERS, FINSET_1, ARYTM_3, CARD_1, SUBSET_1, XBOOLE_0, GLIB_000, RELAT_2, GLIB_001, TREES_1, ZFMISC_1, FUNCT_1, FINSEQ_1, GRAPH_1, ABIAN, XXREAL_0, RELAT_1, RCOMP_1, FUNCOP_1, ARYTM_1, WAYBEL_0, TARSKI, PBOOLE, SETFAM_1, ORDINAL1, NAT_1, GLIB_002, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, SETFAM_1, DOMAIN_1, XCMPLX_0, ABIAN, XXREAL_0, RELAT_1, FUNCT_1, PBOOLE, FUNCT_2, FINSEQ_1, NAT_1, FUNCOP_1, GLIB_000, GLIB_001;
definitions TARSKI;
theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, GLIB_000, GLIB_001, ABIAN, INT_1, JORDAN12, NAT_1, ORDINAL1, PENCIL_1, TARSKI, XBOOLE_0, XCMPLX_1, ZFMISC_1, XREAL_1, XXREAL_0, RELSET_1;
schemes NAT_1, SUBSET_1, GLIB_000;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, INT_1, CARD_1, GLIB_000, ABIAN, GLIB_001, FUNCT_2, PARTFUN1;
constructors HIDDEN, DOMAIN_1, CARD_FIL, GLIB_001, VALUED_1, XXREAL_2, WELLORD2, RELSET_1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities FUNCOP_1, ORDINAL1, CARD_1;
expansions TARSKI;
Lm1:
for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v
Lm2:
for G being _Graph
for v1 being Vertex of G
for e, x, y being object st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
Lm3:
for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2
Lm4:
for G being _Graph
for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
Lm5:
for G1 being non trivial connected _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
Lm6:
for G being _Graph st ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 holds
G is connected
Lm7:
for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds
G is connected
Lm8:
for G being _Graph st G is connected holds
for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G
Lm9:
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
Lm10:
for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected
Lm11:
for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} )
Lm12:
for G1, G2 being _Graph st G1 == G2 holds
G1 .componentSet() = G2 .componentSet()
Lm13:
for G being _Graph
for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G)
Lm14:
for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
Lm15:
for G being _Graph
for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
Lm16:
for G being _Graph
for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
Lm17:
for G being _Graph
for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
Lm18:
for G being _Graph holds
( G is connected iff G .numComponents() = 1 )
Lm19:
for G being connected _Graph
for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
Lm20:
for G being connected _Graph
for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
Lm21:
for G being finite non trivial connected _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
Lm22:
for G being acyclic _Graph
for W being Path of G
for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
Lm23:
for G being finite non trivial acyclic _Graph st the_Edges_of G <> {} holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
Lm24:
for G being finite non trivial Tree-like _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex )