:: GRAPH_1 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
set DomEx = {1,2};
reconsider empty1 = {} as Function of {} ,{1,2} by FUNCT_2:55, RELAT_1:60;
:: deftheorem Def1 defines Graph-like GRAPH_1:def 1 :
Lm1:
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 )
Lm2:
for G being Graph
for x being Element of the Vertices of G holds x in the Vertices of G
:: deftheorem Def2 defines \/ GRAPH_1:def 2 :
:: deftheorem Def3 defines is_sum_of GRAPH_1:def 3 :
:: deftheorem Def4 defines oriented GRAPH_1:def 4 :
:: deftheorem Def5 defines non-multi GRAPH_1:def 5 :
:: deftheorem Def6 defines simple GRAPH_1:def 6 :
:: deftheorem Def7 defines connected GRAPH_1:def 7 :
:: deftheorem Def8 defines finite GRAPH_1:def 8 :
:: deftheorem defines joins GRAPH_1:def 9 :
:: deftheorem defines are_incydent GRAPH_1:def 10 :
:: deftheorem Def11 defines Chain GRAPH_1:def 11 :
Lm3:
for G being Graph holds {} is Chain of G
:: deftheorem Def12 defines oriented GRAPH_1:def 12 :
Lm4:
for G being Graph holds {} is oriented Chain of G
:: deftheorem defines one-to-one GRAPH_1:def 13 :
:: deftheorem GRAPH_1:def 14 :
canceled;
:: deftheorem Def15 defines cyclic GRAPH_1:def 15 :
Lm5:
for G being Graph holds {} is Cycle of G
Lm6:
for G being Graph
for v being set st v in the Edges of G holds
( the Source of G . v in the Vertices of G & the Target of G . v in the Vertices of G )
:: deftheorem GRAPH_1:def 16 :
canceled;
:: deftheorem Def17 defines Subgraph GRAPH_1:def 17 :
:: deftheorem defines VerticesCount GRAPH_1:def 18 :
:: deftheorem defines EdgesCount GRAPH_1:def 19 :
:: deftheorem defines EdgesIn GRAPH_1:def 20 :
:: deftheorem defines EdgesOut GRAPH_1:def 21 :
:: deftheorem defines Degree GRAPH_1:def 22 :
Lm7:
for n being Nat
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
Lm8:
for G being Graph
for H1, H2 being strict Subgraph of G st the Vertices of H1 = the Vertices of H2 & the Edges of H1 = the Edges of H2 holds
H1 = H2
:: deftheorem Def23 defines c= GRAPH_1:def 23 :
Lm9:
for G being Graph
for H being Subgraph of G holds
( the Source of H in PFuncs the Edges of G,the Vertices of G & the Target of H in PFuncs the Edges of G,the Vertices of G )
:: deftheorem Def24 defines bool GRAPH_1:def 24 :
theorem :: GRAPH_1:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: GRAPH_1:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: GRAPH_1:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: GRAPH_1:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: GRAPH_1:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: GRAPH_1:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: GRAPH_1:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: GRAPH_1:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: GRAPH_1:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
G1,
G2,
G3 being
Graph st
G1 c= G2 &
G2 c= G3 holds
G1 c= G3
theorem Th18: :: GRAPH_1:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: GRAPH_1:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: GRAPH_1:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: GRAPH_1:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: GRAPH_1:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
G1,
G,
G2 being
Graph st
G1 c= G &
G2 c= G holds
G1 \/ G2 c= G
theorem :: GRAPH_1:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: GRAPH_1:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: GRAPH_1:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: GRAPH_1:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: GRAPH_1:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: GRAPH_1:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: GRAPH_1:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 