begin
:: deftheorem defines dom GRAPH_1:def 1 :
:: deftheorem defines cod GRAPH_1:def 2 :
:: deftheorem Def3 defines \/ GRAPH_1:def 3 :
:: deftheorem Def4 defines is_sum_of GRAPH_1:def 4 :
:: deftheorem Def5 defines oriented GRAPH_1:def 5 :
:: deftheorem Def6 defines non-multi GRAPH_1:def 6 :
:: deftheorem Def7 defines simple GRAPH_1:def 7 :
:: deftheorem Def8 defines connected GRAPH_1:def 8 :
:: deftheorem Def9 defines finite GRAPH_1:def 9 :
:: deftheorem defines joins GRAPH_1:def 10 :
:: deftheorem defines are_incident GRAPH_1:def 11 :
:: deftheorem Def12 defines Chain GRAPH_1:def 12 :
Lm1:
for G being Graph holds {} is Chain of G
:: deftheorem defines oriented GRAPH_1:def 13 :
:: deftheorem defines one-to-one GRAPH_1:def 14 :
:: deftheorem GRAPH_1:def 15 :
canceled;
:: deftheorem defines cyclic GRAPH_1:def 16 :
:: deftheorem GRAPH_1:def 17 :
canceled;
:: deftheorem Def18 defines Subgraph GRAPH_1:def 18 :
:: deftheorem defines VerticesCount GRAPH_1:def 19 :
:: deftheorem defines EdgesCount GRAPH_1:def 20 :
:: deftheorem defines EdgesIn GRAPH_1:def 21 :
:: deftheorem defines EdgesOut GRAPH_1:def 22 :
:: deftheorem defines Degree GRAPH_1:def 23 :
Lm2:
for n being Element of NAT
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
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
:: deftheorem Def24 defines c= GRAPH_1:def 24 :
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 )
:: deftheorem Def25 defines bool GRAPH_1:def 25 :
theorem
theorem
theorem
theorem
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem
theorem
theorem Th16:
theorem Th17:
for
G1,
G2,
G3 being
Graph st
G1 c= G2 &
G2 c= G3 holds
G1 c= G3
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
for
G1,
G,
G2 being
Graph st
G1 c= G &
G2 c= G holds
G1 \/ G2 c= G
theorem
theorem Th24:
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th31:
theorem
theorem
canceled;
theorem
theorem
theorem
theorem