environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, STRUCT_0, FUNCT_1, GLIB_000, XBOOLE_0, FUNCT_5, RELAT_1, PARTFUN1, RELAT_2, FINSET_1, TREES_2, FINSEQ_1, XXREAL_0, ARYTM_3, TARSKI, CARD_1, FUNCT_2, ZFMISC_1, GRAPH_1, RECDEF_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_5, FINSEQ_1, FINSET_1, PARTFUN1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, XXREAL_0, STRUCT_0;
definitions FUNCT_1, TARSKI;
theorems FUNCT_2, FUNCT_1, PARTFUN1, FINSEQ_1, NAT_1, ZFMISC_1, MCART_1, TARSKI, RELAT_1, FINSEQ_3, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1;
schemes FUNCT_2, TARSKI, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, XREAL_0, FINSEQ_1, ORDINAL1, STRUCT_0, CARD_1, FUNCT_2, RELSET_1, NAT_1;
constructors HIDDEN, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, FUNCT_5, RELSET_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities ;
expansions FUNCT_1, TARSKI;
Lm1:
for G being Graph holds {} is Chain of G
Lm2:
for n being Nat
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
Lm3:
for G being Graph
for H1, H2 being strict Subgraph of G st the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 holds
H1 = H2
Lm4:
for G being Graph
for H being Subgraph of G holds
( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) )
theorem Th17:
for
G1,
G2,
G3 being
Graph st
G1 c= G2 &
G2 c= G3 holds
G1 c= G3
theorem Th22:
for
G,
G1,
G2 being
Graph st
G1 c= G &
G2 c= G holds
G1 \/ G2 c= G