:: Graphs
:: by Krzysztof Hryniewiecki
::
:: Received December 5, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

definition

attr c₁ is strict ;
struct MultiGraphStruct -> 2-sorted ;
aggr MultiGraphStruct(# carrier, carrier', Source, Target #) -> MultiGraphStruct ;
sel Source c₁ -> Function of the carrier' of c₁, the carrier of c₁;
sel Target c₁ -> Function of the carrier' of c₁, the carrier of c₁;

end;

definition

let G be MultiGraphStruct ;
mode Vertex of G is Element of G;
mode Edge of G is Element of the carrier' of G;

end;

registration

cluster non empty non void strict MultiGraphStruct ;
existence
ex b₁ being MultiGraphStruct st
( b₁ is strict & not b₁ is empty & not b₁ is void )

proof end;

end;

definition

mode Graph is non empty MultiGraphStruct ;

end;

definition

let C be non empty non void MultiGraphStruct ;
let f be Edge of C;
func dom f -> Vertex of C equals :: GRAPH_1:def 1
the Source of C . f;
correctness
coherence
the Source of C . f is Vertex of C;
;
func cod f -> Vertex of C equals :: GRAPH_1:def 2
the Target of C . f;
correctness
coherence
the Target of C . f is Vertex of C;
;

end;

:: deftheorem defines dom GRAPH_1:def 1 :
for C being non empty non void MultiGraphStruct
for f being Edge of C holds dom f = the Source of C . f;

:: deftheorem defines cod GRAPH_1:def 2 :
for C being non empty non void MultiGraphStruct
for f being Edge of C holds cod f = the Target of C . f;

definition

let G1, G2 be Graph;
assume that
A1: the Source of G1 tolerates the Source of G2 and
A2: the Target of G1 tolerates the Target of G2 ;
func G1 \/ G2 -> strict Graph means :Def3: :: GRAPH_1:def 3
( the carrier of it = the carrier of G1 \/ the carrier of G2 & the carrier' of it = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of it . v = the Source of G1 . v & the Target of it . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of it . v = the Source of G2 . v & the Target of it . v = the Target of G2 . v ) ) );
existence
ex b₁ being strict Graph st
( the carrier of b₁ = the carrier of G1 \/ the carrier of G2 & the carrier' of b₁ = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b₁ . v = the Source of G1 . v & the Target of b₁ . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b₁ . v = the Source of G2 . v & the Target of b₁ . v = the Target of G2 . v ) ) )

proof end;

uniqueness
for b₁, b₂ being strict Graph st the carrier of b₁ = the carrier of G1 \/ the carrier of G2 & the carrier' of b₁ = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b₁ . v = the Source of G1 . v & the Target of b₁ . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b₁ . v = the Source of G2 . v & the Target of b₁ . v = the Target of G2 . v ) ) & the carrier of b₂ = the carrier of G1 \/ the carrier of G2 & the carrier' of b₂ = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b₂ . v = the Source of G1 . v & the Target of b₂ . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b₂ . v = the Source of G2 . v & the Target of b₂ . v = the Target of G2 . v ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines \/ GRAPH_1:def 3 :
for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
for b₃ being strict Graph holds
( b₃ = G1 \/ G2 iff ( the carrier of b₃ = the carrier of G1 \/ the carrier of G2 & the carrier' of b₃ = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b₃ . v = the Source of G1 . v & the Target of b₃ . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b₃ . v = the Source of G2 . v & the Target of b₃ . v = the Target of G2 . v ) ) ) );

definition

let G, G1, G2 be Graph;
pred G is_sum_of G1,G2 means :Def4: :: GRAPH_1:def 4
( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 );

end;

:: deftheorem Def4 defines is_sum_of GRAPH_1:def 4 :
for G, G1, G2 being Graph holds
( G is_sum_of G1,G2 iff ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ) );

definition

let IT be Graph;
attr IT is oriented means :Def5: :: GRAPH_1:def 5
for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds
x = y;
attr IT is non-multi means :Def6: :: GRAPH_1:def 6
for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds
x = y;
attr IT is simple means :Def7: :: GRAPH_1:def 7
for x being set holds
( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x );
attr IT is connected means :Def8: :: GRAPH_1:def 8
for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 );

end;

:: deftheorem Def5 defines oriented GRAPH_1:def 5 :
for IT being Graph holds
( IT is oriented iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds
x = y );

:: deftheorem Def6 defines non-multi GRAPH_1:def 6 :
for IT being Graph holds
( IT is non-multi iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds
x = y );

:: deftheorem Def7 defines simple GRAPH_1:def 7 :
for IT being Graph holds
( IT is simple iff for x being set holds
( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ) );

:: deftheorem Def8 defines connected GRAPH_1:def 8 :
for IT being Graph holds
( IT is connected iff for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ) );

definition

let IT be MultiGraphStruct ;
attr IT is finite means :Def9: :: GRAPH_1:def 9
( the carrier of IT is finite & the carrier' of IT is finite );

end;

:: deftheorem Def9 defines finite GRAPH_1:def 9 :
for IT being MultiGraphStruct holds
( IT is finite iff ( the carrier of IT is finite & the carrier' of IT is finite ) );

registration

cluster finite MultiGraphStruct ;
existence
ex b₁ being MultiGraphStruct st b₁ is finite

proof end;

cluster non empty oriented non-multi simple connected finite MultiGraphStruct ;
existence
ex b₁ being Graph st
( b₁ is finite & b₁ is non-multi & b₁ is oriented & b₁ is simple & b₁ is connected )

proof end;

end;

registration

let G be finite MultiGraphStruct ;
cluster the carrier of G -> finite ;
coherence
the carrier of G is finite by Def9;
cluster the carrier' of G -> finite ;
coherence
the carrier' of G is finite by Def9;

end;

definition

let G be Graph;
let x, y be Element of the carrier of G;
let v be set ;
pred v joins x,y means :: GRAPH_1:def 10
( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) );

end;

:: deftheorem defines joins GRAPH_1:def 10 :
for G being Graph
for x, y being Element of the carrier of G
for v being set holds
( v joins x,y iff ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ) );

definition

let G be Graph;
let x, y be Element of the carrier of G;
pred x,y are_incident means :: GRAPH_1:def 11
ex v being set st
( v in the carrier' of G & v joins x,y );

end;

:: deftheorem defines are_incident GRAPH_1:def 11 :
for G being Graph
for x, y being Element of the carrier of G holds
( x,y are_incident iff ex v being set st
( v in the carrier' of G & v joins x,y ) );

definition

let G be Graph;
mode Chain of G -> FinSequence means :Def12: :: GRAPH_1:def 12
( ( for n being Element of NAT st 1 <= n & n <= len it holds
it . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len it holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & it . n joins x9,y9 ) ) ) );
existence
ex b₁ being FinSequence st
( ( for n being Element of NAT st 1 <= n & n <= len b₁ holds
b₁ . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len b₁) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b₁ holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & b₁ . n joins x9,y9 ) ) ) )

proof end;

end;

:: deftheorem Def12 defines Chain GRAPH_1:def 12 :
for G being Graph
for b₂ being FinSequence holds
( b₂ is Chain of G iff ( ( for n being Element of NAT st 1 <= n & n <= len b₂ holds
b₂ . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len b₂) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b₂ holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & b₂ . n joins x9,y9 ) ) ) ) );

Lm1: for G being Graph holds {} is Chain of G

proof end;

definition

let G be Graph;
:: original: Chain
redefine mode Chain of G -> FinSequence of the carrier' of G;
coherence
for b₁ being Chain of G holds b₁ is FinSequence of the carrier' of G

proof end;

end;

definition

let G be Graph;
let IT be Chain of G;
attr IT is oriented means :: GRAPH_1:def 13
for n being Element of NAT st 1 <= n & n < len IT holds
the Source of G . (IT . (n + 1)) = the Target of G . (IT . n);

end;

:: deftheorem defines oriented GRAPH_1:def 13 :
for G being Graph
for IT being Chain of G holds
( IT is oriented iff for n being Element of NAT st 1 <= n & n < len IT holds
the Source of G . (IT . (n + 1)) = the Target of G . (IT . n) );

registration

let G be Graph;
cluster Relation-like the carrier' of G -valued Function-like empty finite FinSequence-like FinSubsequence-like Chain of G;
existence
ex b₁ being Chain of G st b₁ is empty

proof end;

end;

registration

let G be Graph;
cluster empty -> oriented Chain of G;
coherence
for b₁ being Chain of G st b₁ is empty holds
b₁ is oriented

proof end;

end;

definition

let G be Graph;
let IT be Chain of G;
:: original: one-to-one
redefine attr IT is one-to-one means :: GRAPH_1:def 14
for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m;
compatibility
( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m )

proof end;

end;

:: deftheorem defines one-to-one GRAPH_1:def 14 :
for G being Graph
for IT being Chain of G holds
( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m );

definition

let G be Graph;
mode Path of G is V7() Chain of G;

end;

definition

let G be Graph;
mode OrientedPath of G is V7() oriented Chain of G;

end;

definition

let G be Graph;
let IT be Path of G;
canceled;
attr IT is cyclic means :: GRAPH_1:def 16
ex p being FinSequence st
( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) );

end;

:: deftheorem GRAPH_1:def 15 :
canceled;

:: deftheorem defines cyclic GRAPH_1:def 16 :
for G being Graph
for IT being Path of G holds
( IT is cyclic iff ex p being FinSequence st
( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ) );

registration

let G be Graph;
cluster one-to-one empty -> cyclic Chain of G;
coherence
for b₁ being Path of G st b₁ is empty holds
b₁ is cyclic

proof end;

end;

definition

let G be Graph;
mode Cycle of G is cyclic Path of G;

end;

definition

let G be Graph;
mode OrientedCycle of G is cyclic OrientedPath of G;

end;

definition

let G be Graph;
canceled;
mode Subgraph of G -> Graph means :Def18: :: GRAPH_1:def 18
( the carrier of it c= the carrier of G & the carrier' of it c= the carrier' of G & ( for v being set st v in the carrier' of it holds
( the Source of it . v = the Source of G . v & the Target of it . v = the Target of G . v & the Source of G . v in the carrier of it & the Target of G . v in the carrier of it ) ) );
existence
ex b₁ being Graph st
( the carrier of b₁ c= the carrier of G & the carrier' of b₁ c= the carrier' of G & ( for v being set st v in the carrier' of b₁ holds
( the Source of b₁ . v = the Source of G . v & the Target of b₁ . v = the Target of G . v & the Source of G . v in the carrier of b₁ & the Target of G . v in the carrier of b₁ ) ) )

proof end;

end;

:: deftheorem GRAPH_1:def 17 :
canceled;

:: deftheorem Def18 defines Subgraph GRAPH_1:def 18 :
for G, b₂ being Graph holds
( b₂ is Subgraph of G iff ( the carrier of b₂ c= the carrier of G & the carrier' of b₂ c= the carrier' of G & ( for v being set st v in the carrier' of b₂ holds
( the Source of b₂ . v = the Source of G . v & the Target of b₂ . v = the Target of G . v & the Source of G . v in the carrier of b₂ & the Target of G . v in the carrier of b₂ ) ) ) );

registration

let G be Graph;
cluster non empty strict Subgraph of G;
existence
ex b₁ being Subgraph of G st b₁ is strict

proof end;

end;

definition

let G be finite Graph;
func VerticesCount G -> Element of NAT means :: GRAPH_1:def 19
ex B being finite set st
( B = the carrier of G & it = card B );
existence
ex b₁ being Element of NAT ex B being finite set st
( B = the carrier of G & b₁ = card B )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex B being finite set st
( B = the carrier of G & b₁ = card B ) & ex B being finite set st
( B = the carrier of G & b₂ = card B ) holds
b₁ = b₂ ;
func EdgesCount G -> Element of NAT means :: GRAPH_1:def 20
ex B being finite set st
( B = the carrier' of G & it = card B );
existence
ex b₁ being Element of NAT ex B being finite set st
( B = the carrier' of G & b₁ = card B )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex B being finite set st
( B = the carrier' of G & b₁ = card B ) & ex B being finite set st
( B = the carrier' of G & b₂ = card B ) holds
b₁ = b₂ ;

end;

:: deftheorem defines VerticesCount GRAPH_1:def 19 :
for G being finite Graph
for b₂ being Element of NAT holds
( b₂ = VerticesCount G iff ex B being finite set st
( B = the carrier of G & b₂ = card B ) );

:: deftheorem defines EdgesCount GRAPH_1:def 20 :
for G being finite Graph
for b₂ being Element of NAT holds
( b₂ = EdgesCount G iff ex B being finite set st
( B = the carrier' of G & b₂ = card B ) );

definition

let G be finite Graph;
let x be Vertex of G;
func EdgesIn x -> Element of NAT means :: GRAPH_1:def 21
ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & it = card X );
existence
ex b₁ being Element of NAT ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b₁ = card X )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b₁ = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b₂ = card X ) holds
b₁ = b₂

proof end;

func EdgesOut x -> Element of NAT means :: GRAPH_1:def 22
ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & it = card X );
existence
ex b₁ being Element of NAT ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b₁ = card X )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b₁ = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b₂ = card X ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines EdgesIn GRAPH_1:def 21 :
for G being finite Graph
for x being Vertex of G
for b₃ being Element of NAT holds
( b₃ = EdgesIn x iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b₃ = card X ) );

:: deftheorem defines EdgesOut GRAPH_1:def 22 :
for G being finite Graph
for x being Vertex of G
for b₃ being Element of NAT holds
( b₃ = EdgesOut x iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b₃ = card X ) );

definition

let G be finite Graph;
let x be Vertex of G;
func Degree x -> Element of NAT equals :: GRAPH_1:def 23
(EdgesIn x) + (EdgesOut x);
correctness
coherence
(EdgesIn x) + (EdgesOut x) is Element of NAT ;
;

end;

:: deftheorem defines Degree GRAPH_1:def 23 :
for G being finite Graph
for x being Vertex of G holds Degree x = (EdgesIn x) + (EdgesOut x);

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

proof end;

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

proof end;

definition

let G1, G2 be Graph;
pred G1 c= G2 means :Def24: :: GRAPH_1:def 24
G1 is Subgraph of G2;
reflexivity
for G1 being Graph holds G1 is Subgraph of G1

proof end;

end;

:: deftheorem Def24 defines c= GRAPH_1:def 24 :
for G1, G2 being Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );

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) )

proof end;

definition

let G be Graph;
func bool G -> set means :Def25: :: GRAPH_1:def 25
for x being set holds
( x in it iff x is strict Subgraph of G );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is strict Subgraph of G )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is strict Subgraph of G ) ) & ( for x being set holds
( x in b₂ iff x is strict Subgraph of G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def25 defines bool GRAPH_1:def 25 :
for G being Graph
for b₂ being set holds
( b₂ = bool G iff for x being set holds
( x in b₂ iff x is strict Subgraph of G ) );

scheme :: GRAPH_1:sch 1
GraphSeparation{ F₁() -> Graph, P₁[ set ] } :

ex X being set st
for x being set holds
( x in X iff ( x is strict Subgraph of F₁() & P₁[x] ) )

proof end;

theorem :: GRAPH_1:1

for G being Graph holds
( dom the Source of G = the carrier' of G & dom the Target of G = the carrier' of G ) by FUNCT_2:def 1;

theorem :: GRAPH_1:2

for G being Graph
for x being Vertex of G holds x in the carrier of G ;

theorem :: GRAPH_1:3

for G being Graph
for v being set st v in the carrier' of G holds
( the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:7;

theorem :: GRAPH_1:4

for n being Element of NAT
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G by Lm2;

theorem Th5: :: GRAPH_1:5

for G1, G being Graph st G1 c= G holds
( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )

proof end;

theorem :: GRAPH_1:6

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 )

proof end;

theorem Th7: :: GRAPH_1:7

for G being strict Graph holds G = G \/ G

proof end;

theorem Th8: :: GRAPH_1:8

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
G1 \/ G2 = G2 \/ G1

proof end;

theorem Th9: :: GRAPH_1:9

for G1, G2, G3 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G3 & the Target of G1 tolerates the Target of G3 & the Source of G2 tolerates the Source of G3 & the Target of G2 tolerates the Target of G3 holds
(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

proof end;

theorem Th10: :: GRAPH_1:10

for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
G is_sum_of G2,G1

proof end;

theorem :: GRAPH_1:11

for G being strict Graph holds G is_sum_of G,G

proof end;

theorem Th12: :: GRAPH_1:12

for G1, G2 being Graph st ex G being Graph st
( G1 c= G & G2 c= G ) holds
G1 \/ G2 = G2 \/ G1

proof end;

theorem :: GRAPH_1:13

for G1, G2, G3 being Graph st ex G being Graph st
( G1 c= G & G2 c= G & G3 c= G ) holds
(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

proof end;

theorem :: GRAPH_1:14

for G being Graph holds {} is Chain of G by Lm1;

theorem :: GRAPH_1:15

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 by Lm3;

theorem Th16: :: GRAPH_1:16

for G1, G2 being strict Graph st G1 c= G2 & G2 c= G1 holds
G1 = G2

proof end;

theorem Th17: :: GRAPH_1:17

for G1, G2, G3 being Graph st G1 c= G2 & G2 c= G3 holds
G1 c= G3

proof end;

theorem Th18: :: GRAPH_1:18

for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
( G1 c= G & G2 c= G )

proof end;

theorem Th19: :: GRAPH_1:19

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

proof end;

theorem Th20: :: GRAPH_1:20

for G1, G2 being Graph st ex G being Graph st
( G1 c= G & G2 c= G ) holds
( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

proof end;

theorem Th21: :: GRAPH_1:21

for G1, G3, G2, G being Graph st G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 holds
G c= G3

proof end;

theorem Th22: :: GRAPH_1:22

for G1, G, G2 being Graph st G1 c= G & G2 c= G holds
G1 \/ G2 c= G

proof end;

theorem :: GRAPH_1:23

for G1, G2 being strict Graph st G1 c= G2 holds
( G1 \/ G2 = G2 & G2 \/ G1 = G2 )

proof end;

theorem Th24: :: GRAPH_1:24

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) holds
G1 c= G2

proof end;

theorem :: GRAPH_1:25

canceled;

theorem :: GRAPH_1:26

canceled;

theorem :: GRAPH_1:27

for G1 being Graph
for G being oriented Graph st G1 c= G holds
G1 is oriented

proof end;

theorem :: GRAPH_1:28

for G1 being Graph
for G being non-multi Graph st G1 c= G holds
G1 is non-multi

proof end;

theorem :: GRAPH_1:29

for G1 being Graph
for G being simple Graph st G1 c= G holds
G1 is simple

proof end;

theorem :: GRAPH_1:30

for G being Graph
for G1 being strict Graph holds
( G1 in bool G iff G1 c= G )

proof end;

theorem Th31: :: GRAPH_1:31

for G being strict Graph holds G in bool G

proof end;

theorem :: GRAPH_1:32

for G2 being Graph
for G1 being strict Graph holds
( G1 c= G2 iff bool G1 c= bool G2 )

proof end;

theorem :: GRAPH_1:33

canceled;

theorem :: GRAPH_1:34

for G being strict Graph holds {G} c= bool G

proof end;

theorem :: GRAPH_1:35

for G1, G2 being strict Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & bool (G1 \/ G2) c= (bool G1) \/ (bool G2) & not G1 c= G2 holds
G2 c= G1

proof end;

theorem :: GRAPH_1:36

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds
(bool G1) \/ (bool G2) c= bool (G1 \/ G2)

proof end;

theorem :: GRAPH_1:37

for G1, G, G2 being Graph st G1 in bool G & G2 in bool G holds
G1 \/ G2 in bool G

proof end;