:: The Formalisation of Simple Graphs
:: by Yozo Toda
::
:: Received September 8, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

Lm1:  for e being set
for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i &amp; 1 <= i &amp; i <= n )
proofend;

:: interval is defined as subset of reals in measure5.
:: so we use a symbol nat_interval here.
:: following the definition of Seg, I add an assumption 1 <= m.
:: but it is unnatural, I think.
:: I changed the proof of existence
:: so that the assumption (1 <= m) is not necessary.
:: now nat_interval has the very natural definition, I think (-:
definition
let m, n be Nat;
func nat_interval (m,n) ->  Subset of NAT equals :: SGRAPH1:def 1
 {  i where i is Element of NAT : ( m <= i &amp; i <= n )  }  ;
coherence
  {  i where i is Element of NAT : ( m <= i &amp; i <= n )  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines nat_interval SGRAPH1:def_1_:_
 for m, n being Nat holds nat_interval (m,n) =  {  i where i is Element of NAT : ( m <= i &amp; i <= n )  }  ;

notation
let m, n be Nat;
synonym  Seg (m,n) for  nat_interval (m,n);
end;

registration
let m, n be Nat;
cluster nat_interval (m,n) ->  finite ;
coherence
 nat_interval (m,n) is finite
proofend;
end;

theorem :: SGRAPH1:1
for m, n being Element of NAT
for e being set holds
( e in nat_interval (m,n) iff ex i being Element of NAT st
( e = i &amp; m <= i &amp; i <= n ) ) ;

theorem :: SGRAPH1:2
for m, n, k being Element of NAT holds
( k in nat_interval (m,n) iff ( m <= k &amp; k <= n ) )
proofend;

theorem :: SGRAPH1:3
for n being Element of NAT holds nat_interval (1,n) = Seg n
proofend;

theorem Th4: :: SGRAPH1:4
for m, n being Element of NAT st 1 <= m holds
nat_interval (m,n) c= Seg n
proofend;

theorem Th5: :: SGRAPH1:5
for k, m, n being Element of NAT st k < m holds
Seg k misses nat_interval (m,n)
proofend;

theorem :: SGRAPH1:6
for m, n being Element of NAT st n < m holds
nat_interval (m,n) = {}
proofend;

Lm2:  for A being set
for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
proofend;

definition
let A be set ;
func TWOELEMENTSETS A ->  set  equals :: SGRAPH1:def 2
 {  z where z is finite Subset of A : card z = 2  }  ;
coherence
  {  z where z is finite Subset of A : card z = 2  }  is set ;
end;

:: deftheorem  defines TWOELEMENTSETS SGRAPH1:def_2_:_
 for A being set holds TWOELEMENTSETS A =  {  z where z is finite Subset of A : card z = 2  }  ;

theorem Th7: :: SGRAPH1:7
for A, e being set holds
( e in TWOELEMENTSETS A iff ex z being finite Subset of A st
( e = z &amp; card z = 2 ) ) ;

theorem Th8: :: SGRAPH1:8
for A, e being set holds
( e in TWOELEMENTSETS A iff ( e is finite Subset of A &amp; ex x, y being set st
( x in A &amp; y in A &amp; x <> y &amp; e = {x,y} ) ) )
proofend;

theorem Th9: :: SGRAPH1:9
for A being set holds TWOELEMENTSETS A c= bool A
proofend;

theorem Th10: :: SGRAPH1:10
for A, e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A &amp; e2 in A &amp; e1 <> e2 )
proofend;

theorem Th11: :: SGRAPH1:11
TWOELEMENTSETS {} = {}
proofend;

theorem :: SGRAPH1:12
for t, u being set st t c= u holds
TWOELEMENTSETS t c= TWOELEMENTSETS u
proofend;

theorem Th13: :: SGRAPH1:13
for A being finite set holds TWOELEMENTSETS A is finite by Th9, FINSET_1:1;

theorem :: SGRAPH1:14
for A being non trivial set holds not TWOELEMENTSETS A is empty
proofend;

theorem :: SGRAPH1:15
for a being set holds TWOELEMENTSETS {a} = {}
proofend;

begin

:: graph is defined as a pair of two sets, of vertices and of edges.
:: we treat only simple graphs;
:: edges are non-directed, there is no loop,
:: between two vertices is at most one edge.
:: we define the set of all graphs SIMPLEGRAPHS,
:: and later define some operations on graphs
:: (contraction, deletion, minor, etc.) as relations on SIMPLEGRAPHS.
:: Vertices and Edges are used in graph_1. so we must use different names.
:: we restrict simple graphs as finite ones
:: to treat degree as a cardinal of a set of edges.
definition
attrc1 is strict ;
struct SimpleGraphStruct  ->  1-sorted ;
aggrSimpleGraphStruct(# carrier, SEdges #) ->  SimpleGraphStruct ;
sel SEdges c1 ->  Subset of (TWOELEMENTSETS the carrier of c1);
end;

:: SIMPLEGRAPHS is the set of all (simple) graphs,
:: which is the smallest set satisfying following three conditions:
:: (1) it contains <Empty,Empty>,
:: (2) if <V,E> is an element of SIMPLEGRAPHS and n is not a vertex of <V,E>,
:: then <(V U {n}),E> is also an element of SIMPLEGRAPHS,
:: (3) if <V,E> is an element of SIMPLEGRAPHS,
:: v1,v2 are different vertices of <V,E>,
:: and {v1,v2} is not an edge of <V,E>,
:: then <V,(E U {v1,v2})> is also an element of SIMPLEGRAPHS.
definition
let X be set ;
func SIMPLEGRAPHS X ->  set  equals :: SGRAPH1:def 3
 {  SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum  }  ;
coherence
  {  SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum  }  is set ;
end;

:: deftheorem  defines SIMPLEGRAPHS SGRAPH1:def_3_:_
 for X being set holds SIMPLEGRAPHS X =  {  SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum  }  ;

theorem Th16: :: SGRAPH1:16
for X being set holds SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X
proofend;

registration
let X be set ;
cluster SIMPLEGRAPHS X ->  non empty ;
coherence
 not SIMPLEGRAPHS X is empty by Th16;
end;

definition
let X be set ;
mode SimpleGraph of X ->  strict SimpleGraphStruct  means :Def4: :: SGRAPH1:def 4
it is Element of SIMPLEGRAPHS X;
existence
 ex b1 being strict SimpleGraphStruct st b1 is Element of SIMPLEGRAPHS X
proofend;
end;

:: deftheorem Def4 defines SimpleGraph SGRAPH1:def_4_:_
 for X being set
for b2 being strict SimpleGraphStruct holds
( b2 is SimpleGraph of X iff b2 is Element of SIMPLEGRAPHS X );

theorem Th17: :: SGRAPH1:17
for X, g being set holds
( g in SIMPLEGRAPHS X iff ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ) ;

begin

theorem Th18: :: SGRAPH1:18
for X being set
for g being SimpleGraph of X holds
( the carrier of g c= X &amp; the SEdges of g c= TWOELEMENTSETS the carrier of g )
proofend;

theorem :: SGRAPH1:19
for X being set
for g being SimpleGraph of X
for e being set st e in the SEdges of g holds
ex v1, v2 being set st
( v1 in the carrier of g &amp; v2 in the carrier of g &amp; v1 <> v2 &amp; e = {v1,v2} ) by Th8;

theorem :: SGRAPH1:20
for X being set
for g being SimpleGraph of X
for v1, v2 being set st {v1,v2} in the SEdges of g holds
( v1 in the carrier of g &amp; v2 in the carrier of g &amp; v1 <> v2 ) by Th10;

theorem Th21: :: SGRAPH1:21
for X being set
for g being SimpleGraph of X holds
( the carrier of g is finite Subset of X &amp; the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )
proofend;

:: SECTION 3: equality relation on SIMPLEGRAPHS.
:: two graphs are said to be "isomorphic" if
:: (1) there is bijective function (i.e. set-theoretic isomorphism)
:: between two sets of vertices,
:: (2) this iso. respects the correspondence of edges.
definition
let X be set ;
let G, G9 be SimpleGraph of X;
predG is_isomorphic_to G9 means :: SGRAPH1:def 5
 ex Fv being Function of the carrier of G, the carrier of G9 st
( Fv is bijective &amp; ( for v1, v2 being Element of G holds
( {v1,v2} in the SEdges of G iff {(Fv . v1),(Fv . v2)} in the SEdges of G ) ) );
end;

:: deftheorem  defines is_isomorphic_to SGRAPH1:def_5_:_
 for X being set
for G, G9 being SimpleGraph of X holds
( G is_isomorphic_to G9 iff ex Fv being Function of the carrier of G, the carrier of G9 st
( Fv is bijective &amp; ( for v1, v2 being Element of G holds
( {v1,v2} in the SEdges of G iff {(Fv . v1),(Fv . v2)} in the SEdges of G ) ) ) );

begin

scheme :: SGRAPH1:sch 1
IndSimpleGraphs0{ F1() ->  set , P1[ set ] } :
 for G being set st G in SIMPLEGRAPHS F1() holds
P1[G]
provided
A1: P1[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)] and
A2: for g being SimpleGraph of F1()
for v being set st g in SIMPLEGRAPHS F1() &amp; P1[g] &amp; v in F1() &amp; not v in the carrier of g holds
P1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] and
A3: for g being SimpleGraph of F1()
for e being set st P1[g] &amp; e in TWOELEMENTSETS the carrier of g &amp; not e in the SEdges of g holds
ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} &amp; P1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proofend;

:: now we give a theorem characterising SIMPLEGRAPHS as
:: an inductively defined set. we need some lemmas.
theorem :: SGRAPH1:22
for X being set
for g being SimpleGraph of X holds
( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty &amp; g = SimpleGraphStruct(# v,e #) ) )
proofend;

theorem Th23: :: SGRAPH1:23
for X being set
for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X &amp; n in X holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
proofend;

theorem Th24: :: SGRAPH1:24
for X being set
for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st v1 in V &amp; v2 in V &amp; v1 <> v2 &amp; SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} &amp; SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
proofend;

:: next we define a predicate
:: which describe how SIMPLEGRAPHS are generated inductively.
:: *** QUESTION ***
:: conditions (not n in V) and (not {v1,v2} in E) are redundant?
definition
let X, GG be set ;
predGG is_SetOfSimpleGraphs_of X means :Def6: :: SGRAPH1:def 6
( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG &amp; ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG &amp; n in X &amp; not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) &amp; ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG &amp; v1 in V &amp; v2 in V &amp; v1 <> v2 &amp; not {v1,v2} in E holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} &amp; SimpleGraphStruct(# V,v1v2 #) in GG ) ) );
end;

:: deftheorem Def6 defines is_SetOfSimpleGraphs_of SGRAPH1:def_6_:_
 for X, GG being set holds
( GG is_SetOfSimpleGraphs_of X iff ( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG &amp; ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG &amp; n in X &amp; not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) &amp; ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG &amp; v1 in V &amp; v2 in V &amp; v1 <> v2 &amp; not {v1,v2} in E holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} &amp; SimpleGraphStruct(# V,v1v2 #) in GG ) ) ) );

theorem Th25: :: SGRAPH1:25
for X being set holds SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
proofend;

theorem Th26: :: SGRAPH1:26
for X, OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER
proofend;

theorem :: SGRAPH1:27
for X being set holds
( SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X &amp; ( for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER ) ) by Th25, Th26;

begin

:: graph G is a subgraph of graph G' if
:: (1) the set of vertices of G is a subset of the set of vertices of G',
:: (2) the set of edges of G is a subset of the set of edges of G',
:: where two endpoints of each edge of G must be the vertices of G.
:: (of course G must be a graph!)
:: now no lemma is proved )-:
definition
let X be set ;
let G be SimpleGraph of X;
mode SubGraph of G ->  SimpleGraph of X means :: SGRAPH1:def 7
( the carrier of it c= the carrier of G &amp; the SEdges of it c= the SEdges of G );
existence
 ex b1 being SimpleGraph of X st
( the carrier of b1 c= the carrier of G &amp; the SEdges of b1 c= the SEdges of G ) ;
end;

:: deftheorem  defines SubGraph SGRAPH1:def_7_:_
 for X being set
for G, b3 being SimpleGraph of X holds
( b3 is SubGraph of G iff ( the carrier of b3 c= the carrier of G &amp; the SEdges of b3 c= the SEdges of G ) );

begin

:: the degree of a vertex means the number of edges connected to that vertex.
:: in the case of simple graphs, we can prove that
:: the degree is equal to the number of adjacent vertices.
:: (if loop is allowed,
:: the number of edges and the number of adjacent vertices are different.)
:: at first we defined degree(v),
:: where v was Element of the SEdges of(G) and G was an implicit argument.
:: but now we have changed the type of v to set,
:: and G must be an explicit argument
:: or we get an error "Inaccessible locus".
definition
let X be set ;
let G be SimpleGraph of X;
let v be set ;
func degree (G,v) ->  Element of NAT  means :Def8: :: SGRAPH1:def 8
 ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G &amp; v in z ) ) ) &amp; it = card X );
existence
 ex b1 being Element of NAT ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G &amp; v in z ) ) ) &amp; b1 = card X )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G &amp; v in z ) ) ) &amp; b1 = card X ) &amp; ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G &amp; v in z ) ) ) &amp; b2 = card X ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines degree SGRAPH1:def_8_:_
 for X being set
for G being SimpleGraph of X
for v being set
for b4 being Element of NAT holds
( b4 = degree (G,v) iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G &amp; v in z ) ) ) &amp; b4 = card X ) );

theorem Th28: :: SGRAPH1:28
for X being non empty set
for G being SimpleGraph of X
for v being set ex ww being finite set st
( ww =  {  w where w is Element of X : ( w in the carrier of G &amp; {v,w} in the SEdges of G )  }  &amp; degree (G,v) = card ww )
proofend;

theorem :: SGRAPH1:29
for X being non empty set
for g being SimpleGraph of X
for v being set st v in the carrier of g holds
ex VV being finite set st
( VV = the carrier of g &amp; degree (g,v) < card VV )
proofend;

theorem :: SGRAPH1:30
for X being set
for g being SimpleGraph of X
for v, e being set st e in the SEdges of g &amp; degree (g,v) = 0 holds
not v in e
proofend;

theorem :: SGRAPH1:31
for X being set
for g being SimpleGraph of X
for v being set
for vg being finite set st vg = the carrier of g &amp; v in vg &amp; 1 + (degree (g,v)) = card vg holds
for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g &amp; e = {v,w} )
proofend;

begin

:: path is coded as a sequence of vertices,
:: any two of them contained are different each other.
:: but the head and the tail may be equal (which is cycle).
definition
let X be set ;
let g be SimpleGraph of X;
let v1, v2 be Element of g;
let p be FinSequence of the carrier of g;
predp is_path_of v1,v2 means :Def9: :: SGRAPH1:def 9
( p . 1 = v1 &amp; p . (len p) = v2 &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) &amp; ( for i, j being Element of NAT st 1 <= i &amp; i < len p &amp; i < j &amp; j < len p holds
( p . i <> p . j &amp; {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) );
end;

:: deftheorem Def9 defines is_path_of SGRAPH1:def_9_:_
 for X being set
for g being SimpleGraph of X
for v1, v2 being Element of g
for p being FinSequence of the carrier of g holds
( p is_path_of v1,v2 iff ( p . 1 = v1 &amp; p . (len p) = v2 &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) &amp; ( for i, j being Element of NAT st 1 <= i &amp; i < len p &amp; i < j &amp; j < len p holds
( p . i <> p . j &amp; {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) ) );

definition
let X be set ;
let g be SimpleGraph of X;
let v1, v2 be Element of the carrier of g;
func PATHS (v1,v2) ->  Subset of ( the carrier of g *) equals :: SGRAPH1:def 10
 {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  ;
coherence
  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  is Subset of ( the carrier of g *)
proofend;
end;

:: deftheorem  defines PATHS SGRAPH1:def_10_:_
 for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g holds PATHS (v1,v2) =  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  ;

theorem :: SGRAPH1:32
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g
for e being set holds
( e in PATHS (v1,v2) iff ex ss being Element of the carrier of g * st
( e = ss &amp; ss is_path_of v1,v2 ) ) ;

theorem :: SGRAPH1:33
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g
for e being Element of the carrier of g * st e is_path_of v1,v2 holds
e in PATHS (v1,v2) ;

::definition :: is_cycle
:: let g be SimpleGraph of X,
:: v1,v2 be Element of (the carrier of g),
:: p be Element of PATHS(v1,v2);
:: pred p is_cycle means :cycleDef:
:: v1=v2 &amp; ex q being Element of ((the carrier of g)*) st (q=p &amp; 3<=(len q));
::end;
definition
let X be set ;
let g be SimpleGraph of X;
let p be set ;
predp is_cycle_of g means :Def11: :: SGRAPH1:def 11
 ex v being Element of the carrier of g st p in PATHS (v,v);
end;

:: deftheorem Def11 defines is_cycle_of SGRAPH1:def_11_:_
 for X being set
for g being SimpleGraph of X
for p being set holds
( p is_cycle_of g iff ex v being Element of the carrier of g st p in PATHS (v,v) );

begin

:: K_{3,3} = {{1,2,3,4,5,6},
:: {{1,4},{1,5},{1,6},{2,4},{2,5},{2,6},{3,4},{3,5},{3,6}}}.
:: K_5 = {{1,2,3,4,5},
:: {{1,2},{1,3},{1,4},{1,5},{2,3},{2,4},{2,5},{3,4},{3,5},{4,5}}}.
:: for the proof of Kuratowski's theorem, we need only K_{3,3} and K_5.
:: here we define complete (and complete bipartate) graphs in general.
definition
let n, m be Element of NAT ;
func K_ (m,n) ->  SimpleGraph of NAT  means :: SGRAPH1:def 12
 ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg m &amp; j in nat_interval ((m + 1),(m + n)) )  }  &amp; it = SimpleGraphStruct(# (Seg (m + n)),ee #) );
existence
 ex b1 being SimpleGraph of NAT ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg m &amp; j in nat_interval ((m + 1),(m + n)) )  }  &amp; b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) )
proofend;
uniqueness
 for b1, b2 being SimpleGraph of NAT st ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg m &amp; j in nat_interval ((m + 1),(m + n)) )  }  &amp; b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) &amp; ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg m &amp; j in nat_interval ((m + 1),(m + n)) )  }  &amp; b2 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) holds
b1 = b2 ;
end;

:: deftheorem  defines K_ SGRAPH1:def_12_:_
 for n, m being Element of NAT
for b3 being SimpleGraph of NAT holds
( b3 = K_ (m,n) iff ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg m &amp; j in nat_interval ((m + 1),(m + n)) )  }  &amp; b3 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) );

definition
let n be Element of NAT ;
func K_ n ->  SimpleGraph of NAT  means :Def13: :: SGRAPH1:def 13
 ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg n &amp; j in Seg n &amp; i <> j )  }  &amp; it = SimpleGraphStruct(# (Seg n),ee #) );
existence
 ex b1 being SimpleGraph of NAT ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg n &amp; j in Seg n &amp; i <> j )  }  &amp; b1 = SimpleGraphStruct(# (Seg n),ee #) )
proofend;
uniqueness
 for b1, b2 being SimpleGraph of NAT st ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg n &amp; j in Seg n &amp; i <> j )  }  &amp; b1 = SimpleGraphStruct(# (Seg n),ee #) ) &amp; ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg n &amp; j in Seg n &amp; i <> j )  }  &amp; b2 = SimpleGraphStruct(# (Seg n),ee #) ) holds
b1 = b2 ;
end;

:: deftheorem Def13 defines K_ SGRAPH1:def_13_:_
 for n being Element of NAT
for b2 being SimpleGraph of NAT holds
( b2 = K_ n iff ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg n &amp; j in Seg n &amp; i <> j )  }  &amp; b2 = SimpleGraphStruct(# (Seg n),ee #) ) );

:: TriangleGraph will be used in the definition of planegraphs.
definition
func TriangleGraph  ->  SimpleGraph of NAT  equals :: SGRAPH1:def 14
 K_ 3;
correctness
coherence
K_ 3 is SimpleGraph of NAT ;
;
end;

:: deftheorem  defines TriangleGraph SGRAPH1:def_14_:_
 TriangleGraph = K_ 3;

theorem Th34: :: SGRAPH1:34
ex ee being Subset of (TWOELEMENTSETS (Seg 3)) st
( ee = {.{.1,2.},{.2,3.},{.3,1.}.} &amp; TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
proofend;

theorem :: SGRAPH1:35
( the carrier of TriangleGraph = Seg 3 &amp; the SEdges of TriangleGraph = {.{.1,2.},{.2,3.},{.3,1.}.} ) by Th34;

theorem :: SGRAPH1:36
( {1,2} in the SEdges of TriangleGraph &amp; {2,3} in the SEdges of TriangleGraph &amp; {3,1} in the SEdges of TriangleGraph ) by Th34, ENUMSET1:def_1;

theorem :: SGRAPH1:37
((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph
proofend;