:: SGRAPH1 semantic presentation

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 & 1 <= i & i <= n )
proof
let e be set ; ::_thesis: for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
let n be Element of NAT ; ::_thesis: ( e in Seg n implies ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) )
assume A1: e in Seg n ; ::_thesis: ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
then reconsider e = e as Element of NAT ;
take  e ; ::_thesis: ( e = e & 1 <= e & e <= n )
thus  ( e = e & 1 <= e & e <= n ) by A1, FINSEQ_1:1; ::_thesis: verum
end;

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 & i <= n )  }  ;
coherence
  {  i where i is Element of NAT : ( m <= i & i <= n )  }  is Subset of NAT
proof
set IT =  {  i where i is Element of NAT : ( m <= i & i <= n )  }  ;
now__::_thesis:_for_e_being_set_st_e_in__{__i_where_i_is_Element_of_NAT_:_(_m_<=_i_&_i_<=_n_)__}__holds_
e_in_{0}_\/_(Seg_n)
let e be set ; ::_thesis: ( e in  {  i where i is Element of NAT : ( m <= i & i <= n )  }  implies e in {0} \/ (Seg n) )
assume  e in  {  i where i is Element of NAT : ( m <= i & i <= n )  }  ; ::_thesis: e in {0} \/ (Seg n)
then consider i being Element of NAT  such that
A1: i = e and
 m <= i and
A2: i <= n ;
now__::_thesis:_e_in_{0}_\/_(Seg_n)
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: e in {0} \/ (Seg n)
then  i in {0} by TARSKI:def_1;
hence  e in {0} \/ (Seg n) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: e in {0} \/ (Seg n)
then  0 + 1 <= i by NAT_1:13;
then  e in Seg n by A1, A2, FINSEQ_1:1;
hence  e in {0} \/ (Seg n) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  e in {0} \/ (Seg n) ; ::_thesis: verum
end;
then A3:  {  i where i is Element of NAT : ( m <= i & i <= n )  }  c= {0} \/ (Seg n) by TARSKI:def_3;
 {0} c= NAT by ZFMISC_1:31;
then  {0} \/ (Seg n) c= NAT by XBOOLE_1:8;
hence   {  i where i is Element of NAT : ( m <= i & i <= n )  }  is Subset of NAT by A3, XBOOLE_1:1; ::_thesis: verum
end;
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 & 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
proof
set IT =  {  i where i is Element of NAT : ( m <= i & i <= n )  }  ;
now__::_thesis:_for_e_being_set_st_e_in__{__i_where_i_is_Element_of_NAT_:_(_m_<=_i_&_i_<=_n_)__}__holds_
e_in_{0}_\/_(Seg_n)
let e be set ; ::_thesis: ( e in  {  i where i is Element of NAT : ( m <= i & i <= n )  }  implies e in {0} \/ (Seg n) )
assume  e in  {  i where i is Element of NAT : ( m <= i & i <= n )  }  ; ::_thesis: e in {0} \/ (Seg n)
then consider i being Element of NAT  such that
A1: i = e and
 m <= i and
A2: i <= n ;
now__::_thesis:_e_in_{0}_\/_(Seg_n)
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: e in {0} \/ (Seg n)
then  i in {0} by TARSKI:def_1;
hence  e in {0} \/ (Seg n) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: e in {0} \/ (Seg n)
then  0 + 1 <= i by NAT_1:13;
then  e in Seg n by A1, A2, FINSEQ_1:1;
hence  e in {0} \/ (Seg n) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  e in {0} \/ (Seg n) ; ::_thesis: verum
end;
then   {  i where i is Element of NAT : ( m <= i & i <= n )  }  c= {0} \/ (Seg n) by TARSKI:def_3;
hence  nat_interval (m,n) is finite ; ::_thesis: verum
end;
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 & m <= i & i <= n ) ) ;

theorem :: SGRAPH1:2
for m, n, k being Element of NAT holds
( k in nat_interval (m,n) iff ( m <= k & k <= n ) )
proof
let m, n, k be Element of NAT ; ::_thesis: ( k in nat_interval (m,n) iff ( m <= k & k <= n ) )
hereby  ::_thesis: ( m <= k & k <= n implies k in nat_interval (m,n) )
assume  k in nat_interval (m,n) ; ::_thesis: ( m <= k & k <= n )
then  ex i being Element of NAT st
( k = i & m <= i & i <= n ) ;
hence  ( m <= k & k <= n ) ; ::_thesis: verum
end;
assume  ( m <= k & k <= n ) ; ::_thesis: k in nat_interval (m,n)
hence  k in nat_interval (m,n) ; ::_thesis: verum
end;

theorem :: SGRAPH1:3
for n being Element of NAT holds nat_interval (1,n) = Seg n
proof
let n be Element of NAT ; ::_thesis: nat_interval (1,n) = Seg n
now__::_thesis:_for_e_being_set_st_e_in_Seg_n_holds_
e_in_nat_interval_(1,n)
let e be set ; ::_thesis: ( e in Seg n implies e in nat_interval (1,n) )
assume A1: e in Seg n ; ::_thesis: e in nat_interval (1,n)
then reconsider i = e as Element of NAT ;
 ( 1 <= i & i <= n ) by A1, FINSEQ_1:1;
hence  e in nat_interval (1,n) ; ::_thesis: verum
end;
then A2: Seg n c= nat_interval (1,n) by TARSKI:def_3;
now__::_thesis:_for_e_being_set_st_e_in_nat_interval_(1,n)_holds_
e_in_Seg_n
let e be set ; ::_thesis: ( e in nat_interval (1,n) implies e in Seg n )
assume  e in nat_interval (1,n) ; ::_thesis: e in Seg n
then  ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) ;
hence  e in Seg n by FINSEQ_1:1; ::_thesis: verum
end;
then  nat_interval (1,n) c= Seg n by TARSKI:def_3;
hence  nat_interval (1,n) = Seg n by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th4: :: SGRAPH1:4
for m, n being Element of NAT st 1 <= m holds
nat_interval (m,n) c= Seg n
proof
let m, n be Element of NAT ; ::_thesis: ( 1 <= m implies nat_interval (m,n) c= Seg n )
assume A1: 1 <= m ; ::_thesis: nat_interval (m,n) c= Seg n
now__::_thesis:_for_e_being_set_st_e_in_nat_interval_(m,n)_holds_
e_in_Seg_n
let e be set ; ::_thesis: ( e in nat_interval (m,n) implies e in Seg n )
assume  e in nat_interval (m,n) ; ::_thesis: e in Seg n
then consider i being Element of NAT  such that
A2: e = i and
A3: m <= i and
A4: i <= n ;
 1 <= i by A1, A3, XXREAL_0:2;
hence  e in Seg n by A2, A4, FINSEQ_1:1; ::_thesis: verum
end;
hence  nat_interval (m,n) c= Seg n by TARSKI:def_3; ::_thesis: verum
end;

theorem Th5: :: SGRAPH1:5
for k, m, n being Element of NAT st k < m holds
Seg k misses nat_interval (m,n)
proof
let k, m, n be Element of NAT ; ::_thesis: ( k < m implies Seg k misses nat_interval (m,n) )
assume A1: k < m ; ::_thesis: Seg k misses nat_interval (m,n)
now__::_thesis:_for_e_being_set_st_e_in_(Seg_k)_/\_(nat_interval_(m,n))_holds_
e_in_{}
let e be set ; ::_thesis: ( e in (Seg k) /\ (nat_interval (m,n)) implies e in {} )
assume A2: e in (Seg k) /\ (nat_interval (m,n)) ; ::_thesis: e in {}
then  e in nat_interval (m,n) by XBOOLE_0:def_4;
then A3: ex j being Element of NAT st
( e = j & m <= j & j <= n ) ;
 e in Seg k by A2, XBOOLE_0:def_4;
then  ex i being Element of NAT st
( e = i & 1 <= i & i <= k ) by Lm1;
hence  e in {} by A1, A3, XXREAL_0:2; ::_thesis: verum
end;
then  (Seg k) /\ (nat_interval (m,n)) c= {} by TARSKI:def_3;
then  (Seg k) /\ (nat_interval (m,n)) = {} ;
hence  Seg k misses nat_interval (m,n) by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: SGRAPH1:6
for m, n being Element of NAT st n < m holds
nat_interval (m,n) = {}
proof
let m, n be Element of NAT ; ::_thesis: ( n < m implies nat_interval (m,n) = {} )
assume A1: n < m ; ::_thesis: nat_interval (m,n) = {}
now__::_thesis:_for_e_being_set_holds_not_e_in_nat_interval_(m,n)
let e be set ; ::_thesis: not e in nat_interval (m,n)
assume  e in nat_interval (m,n) ; ::_thesis: contradiction
then  ex i being Element of NAT st
( e = i & m <= i & i <= n ) ;
hence  contradiction by A1, XXREAL_0:2; ::_thesis: verum
end;
hence  nat_interval (m,n) = {} by XBOOLE_0:def_1; ::_thesis: verum
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
let A be set ; ::_thesis: for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
let s be Subset of A; ::_thesis: for n being set st n in A holds
s \/ {n} is Subset of A
let n be set ; ::_thesis: ( n in A implies s \/ {n} is Subset of A )
assume A1: n in A ; ::_thesis: s \/ {n} is Subset of A
 s \/ {n} c= A
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in s \/ {n} or m in A )
assume A2: m in s \/ {n} ; ::_thesis: m in A
now__::_thesis:_m_in_A
percases ( m in s or m in {n} ) by A2, XBOOLE_0:def_3;
suppose m in s ; ::_thesis: m in A
hence  m in A ; ::_thesis: verum
end;
suppose m in {n} ; ::_thesis: m in A
hence  m in A by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  m in A ; ::_thesis: verum
end;
hence  s \/ {n} is Subset of A ; ::_thesis: verum
end;

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 & card z = 2 ) ) ;

theorem Th8: :: SGRAPH1:8
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
let A, e be set ; ::_thesis: ( 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} ) ) )
hereby  ::_thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) implies e in TWOELEMENTSETS A )
assume  e in TWOELEMENTSETS A ; ::_thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) )
then A1: ex z being finite Subset of A st
( e = z & card z = 2 ) ;
then reconsider e9 = e as finite Subset of A ;
thus  e is finite Subset of A by A1; ::_thesis: ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} )
consider x, y being set  such that
A2: x <> y and
A3: e9 = {x,y} by A1, CARD_2:60;
take x = x; ::_thesis: ex y being set st
( x in A & y in A & x <> y & e = {x,y} )
take y = y; ::_thesis: ( x in A & y in A & x <> y & e = {x,y} )
 ( x in e9 & y in e9 ) by A3, TARSKI:def_2;
hence  ( x in A & y in A ) ; ::_thesis: ( x <> y & e = {x,y} )
thus  ( x <> y & e = {x,y} ) by A2, A3; ::_thesis: verum
end;
assume that
 e is finite Subset of A and
A4: ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) ; ::_thesis: e in TWOELEMENTSETS A
consider x, y being Element of A such that
A5: x in A and
 y in A and
A6: not x = y and
A7: e = {x,y} by A4;
reconsider xy = {x,y} as finite Subset of A by A5, ZFMISC_1:32;
 ex z being finite Subset of A st
( e = z & card z = 2 )
proof
take  xy ; ::_thesis: ( e = xy & card xy = 2 )
thus  e = xy by A7; ::_thesis: card xy = 2
thus  card xy = 2 by A6, CARD_2:57; ::_thesis: verum
end;
hence  e in TWOELEMENTSETS A ; ::_thesis: verum
end;

theorem Th9: :: SGRAPH1:9
for A being set holds TWOELEMENTSETS A c= bool A
proof
let A be set ; ::_thesis: TWOELEMENTSETS A c= bool A
now__::_thesis:_for_x_being_set_st_x_in_TWOELEMENTSETS_A_holds_
x_in_bool_A
let x be set ; ::_thesis: ( x in TWOELEMENTSETS A implies x in bool A )
assume  x in TWOELEMENTSETS A ; ::_thesis: x in bool A
then  x is finite Subset of A by Th8;
hence  x in bool A ; ::_thesis: verum
end;
hence  TWOELEMENTSETS A c= bool A by TARSKI:def_3; ::_thesis: verum
end;

theorem Th10: :: SGRAPH1:10
for A, e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
proof
let A be set ; ::_thesis: for e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
let e1, e2 be set ; ::_thesis: ( {e1,e2} in TWOELEMENTSETS A implies ( e1 in A & e2 in A & e1 <> e2 ) )
assume A1: {e1,e2} in TWOELEMENTSETS A ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then consider x, y being set  such that
A2: ( x in A & y in A & not x = y ) and
A3: {e1,e2} = {x,y} by Th8;
percases ( ( e1 = x & e2 = x ) or ( e1 = x & e2 = y ) or ( e1 = y & e2 = x ) or ( e1 = y & e2 = y ) ) by A3, ZFMISC_1:6;
suppose ( e1 = x & e2 = x ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then  {x} in TWOELEMENTSETS A by A1, ENUMSET1:29;
then  ex x1, x2 being set st
( x1 in A & x2 in A & not x1 = x2 & {x} = {x1,x2} ) by Th8;
hence  ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; ::_thesis: verum
end;
suppose ( e1 = x & e2 = y ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
hence  ( e1 in A & e2 in A & e1 <> e2 ) by A2; ::_thesis: verum
end;
suppose ( e1 = y & e2 = x ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
hence  ( e1 in A & e2 in A & e1 <> e2 ) by A2; ::_thesis: verum
end;
suppose ( e1 = y & e2 = y ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then  {y} in TWOELEMENTSETS A by A1, ENUMSET1:29;
then  ex x1, x2 being set st
( x1 in A & x2 in A & not x1 = x2 & {y} = {x1,x2} ) by Th8;
hence  ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; ::_thesis: verum
end;
end;
end;

theorem Th11: :: SGRAPH1:11
TWOELEMENTSETS {} = {}
proof
 TWOELEMENTSETS {} c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in TWOELEMENTSETS {} or a in {} )
assume  a in TWOELEMENTSETS {} ; ::_thesis: a in {}
then  ex a1, a2 being set st
( a1 in {} & a2 in {} & not a1 = a2 & a = {a1,a2} ) by Th8;
hence  a in {} ; ::_thesis: verum
end;
hence  TWOELEMENTSETS {} = {} ; ::_thesis: verum
end;

theorem :: SGRAPH1:12
for t, u being set st t c= u holds
TWOELEMENTSETS t c= TWOELEMENTSETS u
proof
let t, u be set ; ::_thesis: ( t c= u implies TWOELEMENTSETS t c= TWOELEMENTSETS u )
assume A1: t c= u ; ::_thesis: TWOELEMENTSETS t c= TWOELEMENTSETS u
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in TWOELEMENTSETS t or e in TWOELEMENTSETS u )
assume A2: e in TWOELEMENTSETS t ; ::_thesis: e in TWOELEMENTSETS u
then  e is finite Subset of t by Th8;
then A3: e is finite Subset of u by A1, XBOOLE_1:1;
 ex x, y being set st
( x in t & y in t & not x = y & e = {x,y} ) by A2, Th8;
hence  e in TWOELEMENTSETS u by A1, A3, Th8; ::_thesis: verum
end;

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
proof
let A be non trivial set ; ::_thesis: not TWOELEMENTSETS A is empty
consider a being set  such that
A1: a in A by XBOOLE_0:def_1;
reconsider A9 = A as non empty non trivial set ;
 A9 \ {a} is non empty set by REALSET1:3;
then consider b being set  such that
A2: b in A9 \ {a} by XBOOLE_0:def_1;
 not b in {a} by A2, XBOOLE_0:def_5;
then A3: a <> b by TARSKI:def_1;
 {a,b} c= A by A1, A2, ZFMISC_1:32;
hence  not TWOELEMENTSETS A is empty by A1, A2, A3, Th8; ::_thesis: verum
end;

theorem :: SGRAPH1:15
for a being set holds TWOELEMENTSETS {a} = {}
proof
let a be set ; ::_thesis: TWOELEMENTSETS {a} = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_TWOELEMENTSETS_{a}
let x be set ; ::_thesis: not x in TWOELEMENTSETS {a}
assume  x in TWOELEMENTSETS {a} ; ::_thesis: contradiction
then consider u, v being set  such that
A1: u in {a} and
A2: v in {a} and
A3: u <> v and
 x = {u,v} by Th8;
u = a by A1, TARSKI:def_1
.= v by A2, TARSKI:def_1 ;
hence  contradiction by A3; ::_thesis: verum
end;
hence  TWOELEMENTSETS {a} = {} by XBOOLE_0:def_1; ::_thesis: verum
end;

 begin

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

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
proof
let X be set ; ::_thesis: SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X
reconsider phiv = {} as finite Subset of X by XBOOLE_1:2;
reconsider phie = {} (TWOELEMENTSETS {}) as finite Subset of (TWOELEMENTSETS phiv) ;
 SimpleGraphStruct(# phiv,phie #) in  {  SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum  }  ;
hence  SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X ; ::_thesis: verum
end;

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
proof
take  SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; ::_thesis: SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X
thus  SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X by Th16; ::_thesis: verum
end;
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 & the SEdges of g c= TWOELEMENTSETS the carrier of g )
proof
let X be set ; ::_thesis: for g being SimpleGraph of X holds
( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
let g be SimpleGraph of X; ::_thesis: ( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
 g is Element of SIMPLEGRAPHS X by Def4;
then  ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) by Th17;
hence  the carrier of g c= X ; ::_thesis: the SEdges of g c= TWOELEMENTSETS the carrier of g
thus  the SEdges of g c= TWOELEMENTSETS the carrier of g ; ::_thesis: verum
end;

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 & v2 in the carrier of g & v1 <> v2 & 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 & v2 in the carrier of g & 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 & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )
proof
let X be set ; ::_thesis: 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) )
let g be SimpleGraph of X; ::_thesis: ( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )
 g is Element of SIMPLEGRAPHS X by Def4;
then  ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) by Th17;
hence  ( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) ) ; ::_thesis: verum
end;

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 & ( 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 & ( 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() & 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
let g be set ; ::_thesis: ( g in SIMPLEGRAPHS F1() implies P1[g] )
assume A4: g in SIMPLEGRAPHS F1() ; ::_thesis: P1[g]
then A5: ex v being finite Subset of F1() ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ;
then reconsider G = g as SimpleGraph of F1() by A4, Def4;
A6: the carrier of G c= F1() by Th18;
percases ( F1() is empty or not F1() is empty ) ;
supposeA7: F1() is empty ; ::_thesis: P1[g]
then  the SEdges of G is Subset of {} by A6, Th11;
hence  P1[g] by A1, A6, A7; ::_thesis: verum
end;
suppose not F1() is empty ; ::_thesis: P1[g]
then reconsider X = F1() as non empty set ;
defpred S1[ set ] means P1[ SimpleGraphStruct(# $1,({} (TWOELEMENTSETS $1)) #)];
A8: now__::_thesis:_for_B9_being_Element_of_Fin_X
for_b_being_Element_of_X_st_S1[B9]_&_not_b_in_B9_holds_
S1[B9_\/_{b}]
let B9 be Element of Fin X; ::_thesis: for b being Element of X st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of X; ::_thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
set g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #);
 B9 is finite Subset of X by FINSUB_1:17;
then A9: SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) in SIMPLEGRAPHS F1() ;
then reconsider g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) as SimpleGraph of F1() by Def4;
assume  ( S1[B9] & not b in B9 ) ; ::_thesis: S1[B9 \/ {b}]
then  P1[ SimpleGraphStruct(# ( the carrier of g \/ {b}),({} (TWOELEMENTSETS ( the carrier of g \/ {b}))) #)] by A2, A9;
hence  S1[B9 \/ {b}] ; ::_thesis: verum
end;
A10: S1[ {}. X] by A1;
A11: for VV being Element of Fin X holds S1[VV] from SETWISEO:sch_2(A10, A8);
A12: now__::_thesis:_for_VV_being_Element_of_Fin_X
for_EEa_being_Finite_Subset_of_(TWOELEMENTSETS_VV)
for_EE_being_Subset_of_(TWOELEMENTSETS_VV)_st_EEa_=_EE_holds_
P1[_SimpleGraphStruct(#_VV,EE_#)]
let VV be Element of Fin X; ::_thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
percases ( TWOELEMENTSETS VV = {} or TWOELEMENTSETS VV <> {} ) ;
supposeA13: TWOELEMENTSETS VV = {} ; ::_thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
let EEa be Finite_Subset of (TWOELEMENTSETS VV); ::_thesis: for EE being Subset of (TWOELEMENTSETS VV) st EEa = EE holds
P1[ SimpleGraphStruct(# VV,EE #)]
let EE be Subset of (TWOELEMENTSETS VV); ::_thesis: ( EEa = EE implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume  EEa = EE ; ::_thesis: P1[ SimpleGraphStruct(# VV,EE #)]
 EE = {} (TWOELEMENTSETS VV) by A13;
hence  P1[ SimpleGraphStruct(# VV,EE #)] by A11; ::_thesis: verum
end;
suppose TWOELEMENTSETS VV <> {} ; ::_thesis: for EE being Finite_Subset of (TWOELEMENTSETS EE)
for EE9 being Subset of (TWOELEMENTSETS EE) st b3 = EE9 holds
P1[ SimpleGraphStruct(# EE,b3 #)]
then reconsider TT = TWOELEMENTSETS VV as non empty set ;
defpred S2[ Finite_Subset of TT] means  for EE being Subset of (TWOELEMENTSETS VV) st EE = $1 holds
P1[ SimpleGraphStruct(# VV,EE #)];
A14: now__::_thesis:_for_ee_being_Finite_Subset_of_TT
for_vv_being_Element_of_TT_st_S2[ee]_&_not_vv_in_ee_holds_
S2[ee_\/_{.vv.}]
let ee be Finite_Subset of TT; ::_thesis: for vv being Element of TT st S2[ee] & not vv in ee holds
S2[ee \/ {.vv.}]
let vv be Element of TT; ::_thesis: ( S2[ee] & not vv in ee implies S2[ee \/ {.vv.}] )
assume that
A15: S2[ee] and
A16: not vv in ee ; ::_thesis: S2[ee \/ {.vv.}]
reconsider ee9 = ee as Subset of (TWOELEMENTSETS VV) by FINSUB_1:17;
set g = SimpleGraphStruct(# VV,ee9 #);
 VV is finite Subset of F1() by FINSUB_1:17;
then  SimpleGraphStruct(# VV,ee9 #) is Element of SIMPLEGRAPHS F1() by Th17;
then reconsider g = SimpleGraphStruct(# VV,ee9 #) as SimpleGraph of F1() by Def4;
 P1[g] by A15;
then  ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {vv} & P1[ SimpleGraphStruct(# the carrier of g,sege #)] ) by A3, A16;
hence  S2[ee \/ {.vv.}] ; ::_thesis: verum
end;
A17: S2[ {}. TT]
proof
let EE be Subset of (TWOELEMENTSETS VV); ::_thesis: ( EE = {}. TT implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume  EE = {}. TT ; ::_thesis: P1[ SimpleGraphStruct(# VV,EE #)]
then  EE = {} (TWOELEMENTSETS VV) ;
hence  P1[ SimpleGraphStruct(# VV,EE #)] by A11; ::_thesis: verum
end;
 for EE being Finite_Subset of TT holds S2[EE] from SETWISEO:sch_2(A17, A14);
hence  for EE being Finite_Subset of (TWOELEMENTSETS VV)
for EE9 being Subset of (TWOELEMENTSETS VV) st EE9 = EE holds
P1[ SimpleGraphStruct(# VV,EE9 #)] ; ::_thesis: verum
end;
end;
end;
 ( the carrier of G is Finite_Subset of X & the SEdges of G is Finite_Subset of (TWOELEMENTSETS the carrier of G) ) by A5, FINSUB_1:def_5;
hence  P1[g] by A12; ::_thesis: verum
end;
end;
end;

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 & g = SimpleGraphStruct(# v,e #) ) )
proof
let X be set ; ::_thesis: 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 #) ) )
let g be SimpleGraph of X; ::_thesis: ( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
assume A1: not g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; ::_thesis: ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) )
take  the carrier of g ; ::_thesis: ex e being Subset of (TWOELEMENTSETS the carrier of g) st
( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g,e #) )
take  the SEdges of g ; ::_thesis: ( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) )
thus  not the carrier of g is empty by A1, Th11; ::_thesis: g = SimpleGraphStruct(# the carrier of g, the SEdges of g #)
thus  g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) ; ::_thesis: verum
end;

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 & n in X holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
proof
let X be set ; ::_thesis: 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 holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let V be Subset of X; ::_thesis: 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 holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let E be Subset of (TWOELEMENTSETS V); ::_thesis: for n being set
for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let n be set ; ::_thesis: for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X holds
SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
let Evn be finite Subset of (TWOELEMENTSETS (V \/ {n})); ::_thesis: ( SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X implies SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X and
A2: n in X ; ::_thesis: SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by A1, Def4;
 V = the carrier of g ;
then  V is finite Subset of X by Th21;
then  V \/ {n} is finite Subset of X by A2, Lm2;
hence  SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X ; ::_thesis: verum
end;

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 & 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
let X be set ; ::_thesis: 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 )
let V be Subset of X; ::_thesis: 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 )
let E be Subset of (TWOELEMENTSETS V); ::_thesis: 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 )
let v1, v2 be set ; ::_thesis: ( v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X implies ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: ( v1 in V & v2 in V ) and
A2: not v1 = v2 and
A3: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X ; ::_thesis: ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by A3, Def4;
A4: the SEdges of g is finite Subset of (TWOELEMENTSETS V) by Th21;
 the carrier of g is finite Subset of X by Th21;
then reconsider V = V as finite Subset of X ;
 ( E \/ {{v1,v2}} c= TWOELEMENTSETS V & E \/ {{v1,v2}} is finite )
proof
hereby  :: according to TARSKI:def_3 ::_thesis: E \/ {{v1,v2}} is finite
let e be set ; ::_thesis: ( e in E \/ {{v1,v2}} implies b1 in TWOELEMENTSETS V )
assume A5: e in E \/ {{v1,v2}} ; ::_thesis: b1 in TWOELEMENTSETS V
percases ( e in E or e in {{v1,v2}} ) by A5, XBOOLE_0:def_3;
suppose e in E ; ::_thesis: b1 in TWOELEMENTSETS V
hence  e in TWOELEMENTSETS V ; ::_thesis: verum
end;
suppose e in {{v1,v2}} ; ::_thesis: b1 in TWOELEMENTSETS V
then A6: e = {v1,v2} by TARSKI:def_1;
then  e is Subset of V by A1, ZFMISC_1:32;
hence  e in TWOELEMENTSETS V by A1, A2, A6, Th8; ::_thesis: verum
end;
end;
end;
thus  E \/ {{v1,v2}} is finite by A4; ::_thesis: verum
end;
then reconsider E9 = E \/ {{v1,v2}} as finite Subset of (TWOELEMENTSETS V) ;
 SimpleGraphStruct(# V,E9 #) in SIMPLEGRAPHS X ;
hence  ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) ; ::_thesis: verum
end;

definition
let X, GG be set ;
predGG is_SetOfSimpleGraphs_of X means :Def6: :: SGRAPH1:def 6
( 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 Def6 defines is_SetOfSimpleGraphs_of SGRAPH1:def_6_:_
 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 Th25: :: SGRAPH1:25
for X being set holds SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
proof
let X be set ; ::_thesis: SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
thus  SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X by Th16; :: according to SGRAPH1:def_6 ::_thesis: ( ( 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 ) & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & 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 SIMPLEGRAPHS X ) ) )
thus  for VV being Subset of X
for EE being Subset of (TWOELEMENTSETS VV)
for nn being set
for EEvn being finite Subset of (TWOELEMENTSETS (VV \/ {nn})) st SimpleGraphStruct(# VV,EE #) in SIMPLEGRAPHS X & nn in X & not nn in VV holds
SimpleGraphStruct(# (VV \/ {nn}),EEvn #) in SIMPLEGRAPHS X by Th23; ::_thesis: for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & 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 SIMPLEGRAPHS X )
thus  for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & 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 SIMPLEGRAPHS X ) by Th24; ::_thesis: verum
end;

theorem Th26: :: SGRAPH1:26
for X, OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER
proof
let X, OTHER be set ; ::_thesis: ( OTHER is_SetOfSimpleGraphs_of X implies SIMPLEGRAPHS X c= OTHER )
defpred S1[ set ] means $1 in OTHER;
assume A1: OTHER is_SetOfSimpleGraphs_of X ; ::_thesis: SIMPLEGRAPHS X c= OTHER
A2: for g being SimpleGraph of X
for v being set st g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g holds
S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
proof
let g be SimpleGraph of X; ::_thesis: for v being set st g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g holds
S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
let v be set ; ::_thesis: ( g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g implies S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] )
assume that
 g in SIMPLEGRAPHS X and
A3: ( g in OTHER & v in X & not v in the carrier of g ) ; ::_thesis: S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
set SVg = the carrier of g;
 the carrier of g is Subset of X by Th21;
hence  S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] by A1, A3, Def6; ::_thesis: verum
end;
A4: for g being SimpleGraph of X
for e being set st S1[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} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proof
let g be SimpleGraph of X; ::_thesis: for e being set st S1[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} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
let e be set ; ::_thesis: ( S1[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g implies ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] ) )
assume that
A5: g in OTHER and
A6: e in TWOELEMENTSETS the carrier of g and
A7: not e in the SEdges of g ; ::_thesis: ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
set SVg = the carrier of g;
set SEg = the SEdges of g;
consider v1, v2 being set  such that
A8: ( v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 ) and
A9: e = {v1,v2} by A6, Th8;
 the carrier of g is finite Subset of X by Th21;
then consider v1v2 being finite Subset of (TWOELEMENTSETS the carrier of g) such that
A10: ( v1v2 = the SEdges of g \/ {{v1,v2}} & SimpleGraphStruct(# the carrier of g,v1v2 #) in OTHER ) by A1, A5, A7, A8, A9, Def6;
take  v1v2 ; ::_thesis: ( v1v2 = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,v1v2 #)] )
thus  ( v1v2 = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,v1v2 #)] ) by A9, A10; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in SIMPLEGRAPHS X or e in OTHER )
assume A11: e in SIMPLEGRAPHS X ; ::_thesis: e in OTHER
A12: S1[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)] by A1, Def6;
 for e being set st e in SIMPLEGRAPHS X holds
S1[e] from SGRAPH1:sch_1(A12, A2, A4);
hence  e in OTHER by A11; ::_thesis: verum
end;

theorem :: SGRAPH1:27
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 Th25, Th26;

begin

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 & 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_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 & the SEdges of b3 c= the SEdges of G ) );

begin

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 & v in z ) ) ) & 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 & v in z ) ) ) & b1 = card X )
proof
defpred S1[ set ] means v in $1;
consider X being set  such that
A1: for z being set holds
( z in X iff ( z in the SEdges of G & S1[z] ) ) from XBOOLE_0:sch_1();
A2: X c= the SEdges of G
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in the SEdges of G )
assume  z in X ; ::_thesis: z in the SEdges of G
hence  z in the SEdges of G by A1; ::_thesis: verum
end;
 the SEdges of G is finite by Th21;
then reconsider X = X as finite set by A2;
take  card X ; ::_thesis: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
take  X ; ::_thesis: ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
thus  ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X ) by A1; ::_thesis: verum
end;
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 & 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
let IT1, IT2 be Element of NAT ; ::_thesis: ( ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & IT1 = 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 ) ) ) & IT2 = card X ) implies IT1 = IT2 )
assume  ( ex X1 being finite set st
( ( for z being set holds
( z in X1 iff ( z in the SEdges of G & v in z ) ) ) & IT1 = card X1 ) & ex X2 being finite set st
( ( for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X2 ) ) ; ::_thesis: IT1 = IT2
then consider X1, X2 being finite set  such that
A3: for z being set holds
( z in X1 iff ( z in the SEdges of G & v in z ) ) and
A4: IT1 = card X1 and
A5: for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) and
A6: IT2 = card X2 ;
A7: X2 c= X1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X2 or z in X1 )
assume  z in X2 ; ::_thesis: z in X1
then  ( z in the SEdges of G & v in z ) by A5;
hence  z in X1 by A3; ::_thesis: verum
end;
 X1 c= X2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X1 or z in X2 )
assume  z in X1 ; ::_thesis: z in X2
then  ( z in the SEdges of G & v in z ) by A3;
hence  z in X2 by A5; ::_thesis: verum
end;
hence  IT1 = IT2 by A4, A6, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
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 & v in z ) ) ) & 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 & {v,w} in the SEdges of G )  }  & degree (G,v) = card ww )
proof
let X be non empty set ; ::_thesis: 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 )
let G be SimpleGraph of X; ::_thesis: 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 )
let v be set ; ::_thesis: 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 )
set ww =  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  ;
consider Y being finite set  such that
A1: for z being set holds
( z in Y iff ( z in the SEdges of G & v in z ) ) and
A2: degree (G,v) = card Y by Def8;
A3: for z being set holds
( z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  iff ( z in the carrier of G & {v,z} in the SEdges of G ) )
proof
let z be set ; ::_thesis: ( z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  iff ( z in the carrier of G & {v,z} in the SEdges of G ) )
hereby  ::_thesis: ( z in the carrier of G & {v,z} in the SEdges of G implies z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  )
assume  z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  ; ::_thesis: ( z in the carrier of G & {v,z} in the SEdges of G )
then  ex w being Element of X st
( z = w & w in the carrier of G & {v,w} in the SEdges of G ) ;
hence  ( z in the carrier of G & {v,z} in the SEdges of G ) ; ::_thesis: verum
end;
thus  ( z in the carrier of G & {v,z} in the SEdges of G implies z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  ) ::_thesis: verum
proof
assume A4: ( z in the carrier of G & {v,z} in the SEdges of G ) ; ::_thesis: z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }
 the carrier of G is finite Subset of X by Th21;
hence  z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  by A4; ::_thesis: verum
end;
end;
A5:  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  c= the carrier of G
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  or z in the carrier of G )
assume  z in  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  ; ::_thesis: z in the carrier of G
hence  z in the carrier of G by A3; ::_thesis: verum
end;
 the carrier of G is finite by Th21;
then reconsider ww =  {  w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G )  }  as finite set by A5;
take  ww ; ::_thesis: ( 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 )
 ww,Y are_equipotent
proof
set wwY =  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ;
take   {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds
( not b1 in ww or ex b2 being set st
( b2 in Y & [b1,b2] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) ) ) & ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in ww & [b2,b1] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  or not [b3,b4] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
A6: for x, y, z, u being set st [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  & [z,u] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  holds
( x = z iff y = u )
proof
let x, y, z, u be set ; ::_thesis: ( [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  & [z,u] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  implies ( x = z iff y = u ) )
assume that
A7: [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  and
A8: [z,u] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ; ::_thesis: ( x = z iff y = u )
consider w1 being Element of X such that
A9: [x,y] = [w1,{v,w1}] and
 w1 in ww and
A10: {v,w1} in Y by A7;
consider w2 being Element of X such that
A11: [z,u] = [w2,{v,w2}] and
 w2 in ww and
 {v,w2} in Y by A8;
hereby  ::_thesis: ( y = u implies x = z )
assume A12: x = z ; ::_thesis: y = u
w1 = [x,y] `1 by A9, MCART_1:7
.= z by A12
.= [w2,{v,w2}] `1 by A11, MCART_1:7
.= w2 ;
hence y = [w2,{v,w2}] `2 by A9, MCART_1:7
.= u by A11, MCART_1:7 ;
::_thesis: verum
end;
hereby  ::_thesis: verum
 {v,w1} in the SEdges of G by A1, A10;
then A13: v <> w1 by Th10;
assume A14: y = u ; ::_thesis: x = z
{v,w1} = [x,y] `2 by A9, MCART_1:7
.= u by A14
.= [w2,{v,w2}] `2 by A11, MCART_1:7
.= {v,w2} ;
then  w1 = w2 by A13, ZFMISC_1:6;
hence x = [z,u] `1 by A9, A11, MCART_1:7
.= z ;
::_thesis: verum
end;
end;
A15: for w being set holds
( [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  iff ( w in ww & {v,w} in Y ) )
proof
let w be set ; ::_thesis: ( [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  iff ( w in ww & {v,w} in Y ) )
hereby  ::_thesis: ( w in ww & {v,w} in Y implies [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
assume  [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ; ::_thesis: ( w in ww & {v,w} in Y )
then consider w9 being Element of X such that
A16: [w,{v,w}] = [w9,{v,w9}] and
A17: ( w9 in ww & {v,w9} in Y ) ;
w = [w9,{v,w9}] `1 by A16, MCART_1:7
.= w9 ;
hence  ( w in ww & {v,w} in Y ) by A17; ::_thesis: verum
end;
thus  ( w in ww & {v,w} in Y implies [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) ::_thesis: verum
proof
assume that
A18: w in ww and
A19: {v,w} in Y ; ::_thesis: [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }
A20: w in the carrier of G by A5, A18;
 the carrier of G is finite Subset of X by Th21;
then reconsider w = w as Element of X by A20;
 ex z being Element of X st
( [w,{v,w}] = [z,{v,z}] & z in ww & {v,z} in Y ) by A18, A19;
hence  [w,{v,w}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ; ::_thesis: verum
end;
end;
A21: for y being set st y in Y holds
ex x being set st
( x in ww & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
proof
let y be set ; ::_thesis: ( y in Y implies ex x being set st
( x in ww & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) )
assume A22: y in Y ; ::_thesis: ex x being set st
( x in ww & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
then A23: y in the SEdges of G by A1;
A24: v in y by A1, A22;
 ex w being set st
( w in the carrier of G & y = {v,w} )
proof
consider v1, v2 being set  such that
A25: v1 in the carrier of G and
A26: v2 in the carrier of G and
 v1 <> v2 and
A27: y = {v1,v2} by A23, Th8;
percases ( v = v1 or v = v2 ) by A24, A27, TARSKI:def_2;
supposeA28: v = v1 ; ::_thesis: ex w being set st
( w in the carrier of G & y = {v,w} )
take  v2 ; ::_thesis: ( v2 in the carrier of G & y = {v,v2} )
thus  ( v2 in the carrier of G & y = {v,v2} ) by A26, A27, A28; ::_thesis: verum
end;
supposeA29: v = v2 ; ::_thesis: ex w being set st
( w in the carrier of G & y = {v,w} )
take  v1 ; ::_thesis: ( v1 in the carrier of G & y = {v,v1} )
thus  v1 in the carrier of G by A25; ::_thesis: y = {v,v1}
thus  y = {v,v1} by A27, A29; ::_thesis: verum
end;
end;
end;
then consider w being set  such that
A30: w in the carrier of G and
A31: y = {v,w} ;
take  w ; ::_thesis: ( w in ww & [w,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
thus  w in ww by A3, A23, A30, A31; ::_thesis: [w,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }
hence  [w,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  by A15, A22, A31; ::_thesis: verum
end;
 for x being set st x in ww holds
ex y being set st
( y in Y & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
proof
let x be set ; ::_thesis: ( x in ww implies ex y being set st
( y in Y & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) )
assume A32: x in ww ; ::_thesis: ex y being set st
( y in Y & [x,y] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
take  {v,x} ; ::_thesis: ( {v,x} in Y & [x,{v,x}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  )
A33: v in {v,x} by TARSKI:def_2;
 {v,x} in the SEdges of G by A3, A32;
hence  {v,x} in Y by A1, A33; ::_thesis: [x,{v,x}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }
hence  [x,{v,x}] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  by A15, A32; ::_thesis: verum
end;
hence  ( ( for b1 being set holds
( not b1 in ww or ex b2 being set st
( b2 in Y & [b1,b2] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) ) ) & ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in ww & [b2,b1] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  or not [b3,b4] in  {  [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y )  }  or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) by A21, A6; ::_thesis: verum
end;
hence  ( 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 ) by A2, CARD_1:5; ::_thesis: verum
end;

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 & degree (g,v) < card VV )
proof
let X be non empty set ; ::_thesis: 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 )
let g be SimpleGraph of X; ::_thesis: 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 )
let v be set ; ::_thesis: ( v in the carrier of g implies ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV ) )
reconsider VV = the carrier of g as finite set by Th21;
consider ww being finite set  such that
A1: ww =  {  w where w is Element of X : ( w in VV & {v,w} in the SEdges of g )  }  and
A2: degree (g,v) = card ww by Th28;
assume A3: v in the carrier of g ; ::_thesis: ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
A4: now__::_thesis:_(_ww_=_VV_implies_ww_<>_VV_)
assume  ww = VV ; ::_thesis: ww <> VV
then A5: ex w being Element of X st
( v = w & w in VV & {v,w} in the SEdges of g ) by A3, A1;
 {v,v} = {v} by ENUMSET1:29;
then consider x, y being set  such that
 x in VV and
 y in VV and
A6: x <> y and
A7: {v} = {x,y} by A5, Th8;
 v = x by A7, ZFMISC_1:4;
hence  ww <> VV by A6, A7, ZFMISC_1:4; ::_thesis: verum
end;
take  VV ; ::_thesis: ( VV = the carrier of g & degree (g,v) < card VV )
 ww c= VV
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ww or e in VV )
assume  e in ww ; ::_thesis: e in VV
then  ex w being Element of X st
( e = w & w in VV & {v,w} in the SEdges of g ) by A1;
hence  e in VV ; ::_thesis: verum
end;
then  ww c< VV by A4, XBOOLE_0:def_8;
hence  ( VV = the carrier of g & degree (g,v) < card VV ) by A2, CARD_2:48; ::_thesis: verum
end;

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 & degree (g,v) = 0 holds
not v in e
proof
let X be set ; ::_thesis: for g being SimpleGraph of X
for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds
not v in e
let g be SimpleGraph of X; ::_thesis: for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds
not v in e
let v, e be set ; ::_thesis: ( e in the SEdges of g & degree (g,v) = 0 implies not v in e )
assume that
A1: e in the SEdges of g and
A2: degree (g,v) = 0 ; ::_thesis: not v in e
consider Y being finite set  such that
A3: for z being set holds
( z in Y iff ( z in the SEdges of g & v in z ) ) and
A4: degree (g,v) = card Y by Def8;
assume  v in e ; ::_thesis: contradiction
then  not Y is empty by A1, A3;
hence  contradiction by A2, A4; ::_thesis: verum
end;

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 & 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
let X be set ; ::_thesis: 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} )
let g be SimpleGraph of X; ::_thesis: 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} )
let v be set ; ::_thesis: 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} )
let vg be finite set ; ::_thesis: ( vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg implies for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume that
A1: vg = the carrier of g and
A2: v in vg and
A3: 1 + (degree (g,v)) = card vg ; ::_thesis: for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
 vg is Subset of X by A1, Th21;
then reconsider X = X as non empty set by A2;
let w be Element of vg; ::_thesis: ( v <> w implies ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume A4: v <> w ; ::_thesis: ex e being set st
( e in the SEdges of g & e = {v,w} )
take  {v,w} ; ::_thesis: ( {v,w} in the SEdges of g & {v,w} = {v,w} )
hereby  ::_thesis: {v,w} = {v,w}
now__::_thesis:_{v,w}_in_the_SEdges_of_g
consider ww being finite set  such that
A5: ww =  {  vv where vv is Element of X : ( vv in vg & {v,vv} in the SEdges of g )  }  and
A6: degree (g,v) = card ww by A1, Th28;
reconsider wwv = ww \/ {v} as finite set ;
assume A7: not {v,w} in the SEdges of g ; ::_thesis: contradiction
A8: ( not v in ww & not w in ww )
proof
hereby  ::_thesis: not w in ww
assume  v in ww ; ::_thesis: contradiction
then  ex vv being Element of X st
( v = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
then  {v} in the SEdges of g by ENUMSET1:29;
then  ex z being finite Subset of vg st
( {v} = z & card z = 2 ) by A1, Th7;
hence  contradiction by CARD_1:30; ::_thesis: verum
end;
assume  w in ww ; ::_thesis: contradiction
then  ex vv being Element of X st
( w = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
hence  contradiction by A7; ::_thesis: verum
end;
A9: now__::_thesis:_for_e_being_set_st_e_in_ww_holds_
e_in_vg
let e be set ; ::_thesis: ( e in ww implies e in vg )
assume  e in ww ; ::_thesis: e in vg
then  ex vv being Element of X st
( e = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
hence  e in vg ; ::_thesis: verum
end;
 ( wwv c= vg & wwv <> vg )
proof
 for e being set st e in {v} holds
e in vg by A2, TARSKI:def_1;
then A10: {v} c= vg by TARSKI:def_3;
 ww c= vg by A9, TARSKI:def_3;
hence  wwv c= vg by A10, XBOOLE_1:8; ::_thesis: wwv <> vg
assume A11: wwv = vg ; ::_thesis: contradiction
 not w in {v} by A4, TARSKI:def_1;
hence  contradiction by A8, A11, XBOOLE_0:def_3; ::_thesis: verum
end;
then A12: wwv c< vg by XBOOLE_0:def_8;
 card wwv = 1 + (card ww) by A8, CARD_2:41;
hence  contradiction by A3, A6, A12, CARD_2:48; ::_thesis: verum
end;
hence  {v,w} in the SEdges of g ; ::_thesis: verum
end;
thus  {v,w} = {v,w} ; ::_thesis: verum
end;

begin

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 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of 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 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 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds
{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of 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 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 *)
proof
set IT =  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  ;
  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  c= the carrier of g *
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  or e in the carrier of g * )
assume  e in  {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  ; ::_thesis: e in the carrier of g *
then  ex ss being Element of the carrier of g * st
( e = ss & ss is_path_of v1,v2 ) ;
hence  e in the carrier of g * ; ::_thesis: verum
end;
hence   {  ss where ss is Element of the carrier of g * : ss is_path_of v1,v2  }  is Subset of ( the carrier of g *) ; ::_thesis: verum
end;
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 & 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
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

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 & 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
set VV = Seg (m + n);
set V1 = Seg m;
set V2 = nat_interval ((m + 1),(m + n));
set EE =  {  {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) )  }  ;
 m <= m + n by NAT_1:11;
then A1: Seg m c= Seg (m + n) by FINSEQ_1:5;
A2: nat_interval ((m + 1),(m + n)) c= Seg (m + n) by Th4, NAT_1:11;
  {  {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) )  }  c= TWOELEMENTSETS (Seg (m + n))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) )  }  or e in TWOELEMENTSETS (Seg (m + n)) )
assume  e in  {  {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) )  }  ; ::_thesis: e in TWOELEMENTSETS (Seg (m + n))
then consider i0, j0 being Element of NAT  such that
A3: e = {i0,j0} and
A4: ( i0 in Seg m & j0 in nat_interval ((m + 1),(m + n)) ) ;
 ( i0 in Seg (m + n) & j0 in Seg (m + n) ) by A1, A2, A4;
then  for e0 being set st e0 in e holds
e0 in Seg (m + n) by A3, TARSKI:def_2;
then A5: e c= Seg (m + n) by TARSKI:def_3;
 m < m + 1 by NAT_1:13;
then  Seg m misses nat_interval ((m + 1),(m + n)) by Th5;
then  (Seg m) /\ (nat_interval ((m + 1),(m + n))) = {} by XBOOLE_0:def_7;
then  i0 <> j0 by A4, XBOOLE_0:def_4;
hence  e in TWOELEMENTSETS (Seg (m + n)) by A1, A2, A3, A4, A5, Th8; ::_thesis: verum
end;
then reconsider EE =  {  {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) )  }  as finite Subset of (TWOELEMENTSETS (Seg (m + n))) by Th13, FINSET_1:1;
set IT = SimpleGraphStruct(# (Seg (m + n)),EE #);
 SimpleGraphStruct(# (Seg (m + n)),EE #) in SIMPLEGRAPHS NAT ;
then reconsider IT = SimpleGraphStruct(# (Seg (m + n)),EE #) as SimpleGraph of NAT by Def4;
reconsider EE = EE as Subset of (TWOELEMENTSETS (Seg (m + n))) ;
take  IT ; ::_thesis: 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 #) )
take  EE ; ::_thesis: ( 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 #) )
thus  ( 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 #) ) ; ::_thesis: verum
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  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 & j in nat_interval ((m + 1),(m + n)) )  }  & 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 & 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
set EE =  {  {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j )  }  ;
now__::_thesis:_for_e_being_set_st_e_in__{__{i,j}_where_i,_j_is_Element_of_NAT_:_(_i_in_Seg_n_&_j_in_Seg_n_&_i_<>_j_)__}__holds_
e_in_TWOELEMENTSETS_(Seg_n)
let e be set ; ::_thesis: ( e in  {  {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j )  }  implies e in TWOELEMENTSETS (Seg n) )
assume  e in  {  {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j )  }  ; ::_thesis: e in TWOELEMENTSETS (Seg n)
then consider i0, j0 being Element of NAT  such that
A1: e = {i0,j0} and
A2: i0 in Seg n and
A3: j0 in Seg n and
A4: i0 <> j0 ;
 e c= Seg n
proof
let e0 be set ; :: according to TARSKI:def_3 ::_thesis: ( not e0 in e or e0 in Seg n )
assume A5: e0 in e ; ::_thesis: e0 in Seg n
percases ( e0 = i0 or e0 = j0 ) by A1, A5, TARSKI:def_2;
suppose e0 = i0 ; ::_thesis: e0 in Seg n
hence  e0 in Seg n by A2; ::_thesis: verum
end;
suppose e0 = j0 ; ::_thesis: e0 in Seg n
hence  e0 in Seg n by A3; ::_thesis: verum
end;
end;
end;
hence  e in TWOELEMENTSETS (Seg n) by A1, A2, A3, A4, Th8; ::_thesis: verum
end;
then   {  {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j )  }  c= TWOELEMENTSETS (Seg n) by TARSKI:def_3;
then reconsider EE =  {  {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j )  }  as finite Subset of (TWOELEMENTSETS (Seg n)) by Th13, FINSET_1:1;
set IT = SimpleGraphStruct(# (Seg n),EE #);
 SimpleGraphStruct(# (Seg n),EE #) in SIMPLEGRAPHS NAT ;
then reconsider IT = SimpleGraphStruct(# (Seg n),EE #) as SimpleGraph of NAT by Def4;
take  IT ; ::_thesis: 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 #) )
take  EE ; ::_thesis: ( 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 #) )
thus  ( 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 #) ) ; ::_thesis: verum
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 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 & j in Seg n & i <> j )  }  & b2 = SimpleGraphStruct(# (Seg n),ee #) ) );

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.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
proof
consider ee being finite Subset of (TWOELEMENTSETS (Seg 3)) such that
A1: ee =  {  {i,j} where i, j is Element of NAT : ( i in Seg 3 & j in Seg 3 & i <> j )  }  and
A2: TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) by Def13;
take  ee ; ::_thesis: ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
now__::_thesis:_for_a_being_set_st_a_in_ee_holds_
a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
let a be set ; ::_thesis: ( a in ee implies b1 in {.{.1,2.},{.2,3.},{.3,1.}.} )
assume  a in ee ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
then consider i, j being Element of NAT  such that
A3: a = {i,j} and
A4: i in Seg 3 and
A5: j in Seg 3 and
A6: i <> j by A1;
percases ( i = 1 or i = 2 or i = 3 ) by A4, ENUMSET1:def_1, FINSEQ_3:1;
supposeA7: i = 1 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A7; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
supposeA8: i = 2 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A8; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
supposeA9: i = 3 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A9; ::_thesis: verum
end;
end;
end;
hence  a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
end;
end;
then A10: ee c= {.{.1,2.},{.2,3.},{.3,1.}.} by TARSKI:def_3;
now__::_thesis:_for_e_being_set_st_e_in_{.{.1,2.},{.2,3.},{.3,1.}.}_holds_
e_in_ee
let e be set ; ::_thesis: ( e in {.{.1,2.},{.2,3.},{.3,1.}.} implies b1 in ee )
assume A11: e in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: b1 in ee
percases ( e = {1,2} or e = {2,3} or e = {3,1} ) by A11, ENUMSET1:def_1;
supposeA12: e = {1,2} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 1; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 2; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus  e = {i,j} by A12; ::_thesis: ( i in Seg 3 & j in Seg 3 & i <> j )
thus  ( i in Seg 3 & j in Seg 3 ) by ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: i <> j
thus  i <> j ; ::_thesis: verum
end;
hence  e in ee by A1; ::_thesis: verum
end;
supposeA13: e = {2,3} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 2; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 3; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus  ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A13, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
hence  e in ee by A1; ::_thesis: verum
end;
supposeA14: e = {3,1} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 3; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 1; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus  ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A14, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
hence  e in ee by A1; ::_thesis: verum
end;
end;
end;
then  {.{.1,2.},{.2,3.},{.3,1.}.} c= ee by TARSKI:def_3;
hence  ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) ) by A2, A10, XBOOLE_0:def_10; ::_thesis: verum
end;

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

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

theorem :: SGRAPH1:37
((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph
proof
reconsider o = 1 as Element of the carrier of TriangleGraph by Th34, ENUMSET1:def_1, FINSEQ_3:1;
reconsider VERTICES = the carrier of TriangleGraph as non empty set by Th34;
set p = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>;
A1: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 1 = 1 by FINSEQ_1:66;
reconsider One = 1, Two = 2, Three = 3 as Element of VERTICES by Th34, ENUMSET1:def_1, FINSEQ_3:1;
A2: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 2 = 2 by FINSEQ_1:66;
reconsider ONE = <*One*>, TWO = <*Two*>, THREE = <*Three*> as FinSequence of the carrier of TriangleGraph ;
 ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> = ((ONE ^ TWO) ^ THREE) ^ ONE ;
then reconsider pp = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> as Element of the carrier of TriangleGraph * by FINSEQ_1:def_11;
A3: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 3 = 3 by FINSEQ_1:66;
A4: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 4 = 1 by FINSEQ_1:66;
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_(((<*1*>_^_<*2*>)_^_<*3*>)_^_<*1*>)_holds_
{(pp_._i),(pp_._(i_+_1))}_in_the_SEdges_of_TriangleGraph
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) implies {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph )
assume that
A6: 1 <= i and
A7: i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
 i < 3 + 1 by A7, FINSEQ_1:66;
then  i <= 3 by NAT_1:13;
then A8: i in Seg 3 by A6, FINSEQ_1:1;
percases ( i = 1 or i = 2 or i = 3 ) by A8, ENUMSET1:def_1, FINSEQ_3:1;
suppose i = 1 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence  {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, A2, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
suppose i = 2 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence  {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A2, A3, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence  {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A3, A4, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
A9: now__::_thesis:_for_i,_j_being_Element_of_NAT_st_1_<=_i_&_i_<_len_pp_&_i_<_j_&_j_<_len_pp_holds_
(_pp_._i_<>_pp_._j_&_{(pp_._i),(pp_._(i_+_1))}_<>_{(pp_._j),(pp_._(j_+_1))}_)
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < len pp & i < j & j < len pp implies ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} ) )
assume that
A10: 1 <= i and
A11: i < len pp and
A12: i < j and
A13: j < len pp ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
A14: i + 1 <= j by A12, NAT_1:13;
 i < 3 + 1 by A11, FINSEQ_1:66;
then  i <= 3 by NAT_1:13;
then A15: i in Seg 3 by A10, FINSEQ_1:1;
A16: j < 3 + 1 by A13, FINSEQ_1:66;
then A17: j <= 3 by NAT_1:13;
percases ( i = 1 or i = 2 or i = 3 ) by A15, ENUMSET1:def_1, FINSEQ_3:1;
supposeA18: i = 1 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
then A19: pp . i = o by FINSEQ_1:66;
 ( j = 2 or ( 2 < j & j <= 3 ) ) by A16, A14, A18, NAT_1:13, XXREAL_0:1;
then A20: ( j = 2 or ( 2 + 1 <= j & j <= 3 ) ) by NAT_1:13;
now__::_thesis:_(_pp_._i_<>_pp_._j_&_{(pp_._i),(pp_._(i_+_1))}_<>_{(pp_._j),(pp_._(j_+_1))}_)
percases ( j = 2 or j = 3 ) by A20, XXREAL_0:1;
supposeA21: j = 2 ; ::_thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence  pp . i <> pp . j by A19, FINSEQ_1:66; ::_thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus  {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A21, ZFMISC_1:6; ::_thesis: verum
end;
supposeA22: j = 3 ; ::_thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence  pp . i <> pp . j by A19, FINSEQ_1:66; ::_thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus  {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A22, ZFMISC_1:6; ::_thesis: verum
end;
end;
end;
hence  ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) ; ::_thesis: verum
end;
supposeA23: i = 2 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
then  j = 3 by A14, A17, XXREAL_0:1;
hence  ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A2, A3, A4, A23, ZFMISC_1:6; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
hence  ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A12, A16, NAT_1:13; ::_thesis: verum
end;
end;
end;
 len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) = 4 by FINSEQ_1:66;
then  pp is_path_of o,o by A1, A4, A5, A9, Def9;
then  pp in PATHS (o,o) ;
hence  ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph by Def11; ::_thesis: verum
end;