:: SGRAPH1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for e being set
for n being Nat st e in Seg n holds
ex i being Nat st
( e = i & 1 <= i & i <= n )
proof end;

definition
let m, n be natural number ;
func nat_interval m,n -> Subset of NAT equals :: SGRAPH1:def 1
{ i where i is Nat : ( m <= i & i <= n ) } ;
coherence
{ i where i is Nat : ( m <= i & i <= n ) } is Subset of NAT
proof end;
end;

:: deftheorem defines nat_interval SGRAPH1:def 1 :
for m, n being natural number holds nat_interval m,n = { i where i is Nat : ( m <= i & i <= n ) } ;

notation
let m, n be natural number ;
synonym Seg m,n for nat_interval m,n;
end;

registration
let m, n be natural number ;
cluster nat_interval m,n -> finite ;
coherence
nat_interval m,n is finite
proof end;
end;

theorem :: SGRAPH1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SGRAPH1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for e being set holds
( e in nat_interval m,n iff ex i being Nat st
( e = i & m <= i & i <= n ) ) ;

theorem :: SGRAPH1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, k being Nat holds
( k in nat_interval m,n iff ( m <= k & k <= n ) )
proof end;

theorem :: SGRAPH1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds nat_interval 1,n = Seg n
proof end;

theorem Th5: :: SGRAPH1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st 1 <= m holds
nat_interval m,n c= Seg n
proof end;

theorem Th6: :: SGRAPH1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m, n being Nat st k < m holds
Seg k misses nat_interval m,n
proof end;

theorem :: SGRAPH1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st n < m holds
nat_interval m,n = {}
proof end;

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
proof end;

definition
let A be set ;
canceled;
canceled;
func TWOELEMENTSETS A -> set equals :: SGRAPH1:def 4
{ 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 SGRAPH1:def 2 :
canceled;

:: deftheorem SGRAPH1:def 3 :
canceled;

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

theorem :: SGRAPH1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: SGRAPH1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, e being set holds
( e in TWOELEMENTSETS A iff ex z being finite Subset of A st
( e = z & card z = 2 ) ) ;

theorem Th10: :: SGRAPH1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, e being set holds
( e in TWOELEMENTSETS A iff ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) ) )
proof end;

theorem Th11: :: SGRAPH1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds TWOELEMENTSETS A c= bool A
proof end;

theorem Th12: :: SGRAPH1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
proof end;

theorem Th13: :: SGRAPH1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
TWOELEMENTSETS {} = {}
proof end;

theorem :: SGRAPH1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t, u being set st t c= u holds
TWOELEMENTSETS t c= TWOELEMENTSETS u
proof end;

theorem Th15: :: SGRAPH1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite set holds TWOELEMENTSETS A is finite
proof end;

theorem :: SGRAPH1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non trivial set holds not TWOELEMENTSETS A is empty
proof end;

theorem :: SGRAPH1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds TWOELEMENTSETS {a} = {}
proof end;

registration
let X be empty set ;
cluster -> empty Element of bool X;
coherence
for b1 being Subset of X holds b1 is empty
by XBOOLE_1:3;
end;

definition
attr c1 is strict;
struct SimpleGraphStruct -> 1-sorted ;
aggr SimpleGraphStruct(# carrier, SEdges #) -> SimpleGraphStruct ;
sel SEdges c1 -> Subset of (TWOELEMENTSETS the carrier of c1);
end;

definition
let X be set ;
canceled;
func SIMPLEGRAPHS X -> set equals :: SGRAPH1:def 6
{ 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 SGRAPH1:def 5 :
canceled;

:: deftheorem defines SIMPLEGRAPHS SGRAPH1:def 6 :
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 :: SGRAPH1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: SGRAPH1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in SIMPLEGRAPHS X
proof end;

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

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

:: deftheorem Def7 defines SimpleGraph SGRAPH1:def 7 :
for X being set
for b2 being strict SimpleGraphStruct holds
( b2 is SimpleGraph of X iff b2 is Element of SIMPLEGRAPHS X );

theorem :: SGRAPH1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: SGRAPH1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 #) ) ;

theorem :: SGRAPH1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: SGRAPH1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for g being SimpleGraph of X holds
( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
proof end;

theorem :: SGRAPH1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SGRAPH1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & v2 in the carrier of g & v1 <> v2 & e = {v1,v2} ) by Th10;

theorem :: SGRAPH1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & v2 in the carrier of g & v1 <> v2 ) by Th12;

theorem Th27: :: SGRAPH1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for g being SimpleGraph of X holds
( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )
proof end;

definition
let X be set ;
let G, G' be SimpleGraph of X;
pred G is_isomorphic_to G' means :: SGRAPH1:def 8
ex Fv being Function of the carrier of G,the carrier of G' st
( Fv is bijective & ( 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 8 :
for X being set
for G, G' being SimpleGraph of X holds
( G is_isomorphic_to G' iff ex Fv being Function of the carrier of G,the carrier of G' st
( Fv is bijective & ( 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 ) ) ) );

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() & P1[g] & v in F1() & 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] & e in TWOELEMENTSETS the carrier of g & 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} & P1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proof end;

theorem :: SGRAPH1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & g = SimpleGraphStruct(# v,e #) ) )
proof end;

theorem :: SGRAPH1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th30: :: SGRAPH1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & n in X & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
proof end;

theorem Th31: :: SGRAPH1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
proof end;

definition
let X, GG be set ;
pred GG is_SetOfSimpleGraphs_of X means :Def9: :: SGRAPH1:def 9
( SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in GG & ( 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 & n in X & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) );
end;

:: deftheorem Def9 defines is_SetOfSimpleGraphs_of SGRAPH1:def 9 :
for X, GG being set holds
( GG is_SetOfSimpleGraphs_of X iff ( SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in GG & ( 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 & n in X & not n in V holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) ) );

theorem :: SGRAPH1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SGRAPH1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SGRAPH1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th35: :: SGRAPH1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
proof end;

theorem Th36: :: SGRAPH1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER
proof end;

theorem :: SGRAPH1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X & ( for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER ) ) by Th35, Th36;

definition
let X be set ;
let G be SimpleGraph of X;
mode SubGraph of G -> SimpleGraph of X means :: SGRAPH1:def 10
( the carrier of it c= the carrier of G & 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 & the SEdges of b1 c= the SEdges of G )
;
end;

:: deftheorem defines SubGraph SGRAPH1:def 10 :
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 & the SEdges of b3 c= the SEdges of G ) );

definition
let X be set ;
let G be SimpleGraph of X;
let v be set ;
func degree G,v -> Nat means :Def11: :: SGRAPH1:def 11
ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & it = card X );
existence
ex b1 being Nat ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b1 = card X )
proof end;
uniqueness
for b1, b2 being Nat st ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b1 = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b2 = card X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines degree SGRAPH1:def 11 :
for X being set
for G being SimpleGraph of X
for v being set
for b4 being 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 & v in z ) ) ) & b4 = card X ) );

theorem :: SGRAPH1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th39: :: SGRAPH1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & {v,w} in the SEdges of G ) } & degree G,v = card ww )
proof end;

theorem :: SGRAPH1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & degree g,v < card VV )
proof end;

theorem :: SGRAPH1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for g being SimpleGraph of X
for v, e being set st v in the carrier of g & e in the SEdges of g & degree g,v = 0 holds
not v in e
proof end;

theorem :: SGRAPH1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & v in vg & 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 & e = {v,w} )
proof end;

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;
pred p is_path_of v1,v2 means :Def12: :: SGRAPH1:def 12
( p . 1 = v1 & p . (len p) = v2 & ( for i being Nat st 1 <= i & i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Nat st 1 <= i & i < len p & i < j & j < len p holds
( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) );
end;

:: deftheorem Def12 defines is_path_of SGRAPH1:def 12 :
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 & p . (len p) = v2 & ( for i being Nat st 1 <= i & i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Nat st 1 <= i & i < len p & i < j & j < len p holds
( p . i <> p . j & {(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 13
{ 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 * )
proof end;
end;

:: deftheorem defines PATHS SGRAPH1:def 13 :
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:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SGRAPH1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ss is_path_of v1,v2 ) ) ;

theorem :: SGRAPH1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
let X be set ;
let g be SimpleGraph of X;
let p be set ;
pred p is_cycle_of g means :Def14: :: SGRAPH1:def 14
ex v being Element of the carrier of g st p in PATHS v,v;
end;

:: deftheorem Def14 defines is_cycle_of SGRAPH1:def 14 :
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 );

definition
let n, m be Nat;
canceled;
func K_ m,n -> SimpleGraph of NAT means :: SGRAPH1:def 16
ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval (m + 1),(m + n) ) } & 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 & j in nat_interval (m + 1),(m + n) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) )
proof end;
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 & j in nat_interval (m + 1),(m + n) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) & ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval (m + 1),(m + n) ) } & b2 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) holds
b1 = b2
;
end;

:: deftheorem SGRAPH1:def 15 :
canceled;

:: deftheorem defines K_ SGRAPH1:def 16 :
for n, m being 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 & j in nat_interval (m + 1),(m + n) ) } & b3 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) );

definition
let n be Nat;
func K_ n -> SimpleGraph of NAT means :Def17: :: SGRAPH1:def 17
ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & 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 & j in Seg n & i <> j ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) )
proof end;
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 & j in Seg n & i <> j ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) ) & ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st
( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b2 = SimpleGraphStruct(# (Seg n),ee #) ) holds
b1 = b2
;
end;

:: deftheorem Def17 defines K_ SGRAPH1:def 17 :
for n being 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 & j in Seg n & i <> j ) } & b2 = SimpleGraphStruct(# (Seg n),ee #) ) );

definition
func TriangleGraph -> SimpleGraph of NAT equals :: SGRAPH1:def 18
K_ 3;
correctness
coherence
K_ 3 is SimpleGraph of NAT
;
;
end;

:: deftheorem defines TriangleGraph SGRAPH1:def 18 :
TriangleGraph = K_ 3;

theorem Th46: :: SGRAPH1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex ee being Subset of (TWOELEMENTSETS (Seg 3)) st
( ee = {{1,2},{2,3},{3,1}} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
proof end;

theorem :: SGRAPH1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of TriangleGraph = Seg 3 & the SEdges of TriangleGraph = {{1,2},{2,3},{3,1}} ) by Th46;

theorem :: SGRAPH1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( {1,2} in the SEdges of TriangleGraph & {2,3} in the SEdges of TriangleGraph & {3,1} in the SEdges of TriangleGraph ) by Th46, ENUMSET1:def 1;

theorem :: SGRAPH1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph
proof end;