let G be _finite _Graph; for H being spanning Subgraph of G ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
defpred S1[ Nat] means for H being spanning Subgraph of G st (G .size()) - (H .size()) = $1 holds
ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) );
A1:
S1[ 0 ]
proof
let H be
spanning Subgraph of
G;
( (G .size()) - (H .size()) = 0 implies ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) )
assume A2:
(G .size()) - (H .size()) = 0
;
ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
then A3:
G == H
by Th13;
reconsider p =
<*G*> as non
empty Graph-yielding _finite FinSequence ;
take
p
;
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
thus
p . 1
== H
by A3, FINSEQ_1:40;
( p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
thus p . (len p) =
p . 1
by FINSEQ_1:40
.=
G
by FINSEQ_1:40
;
( len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
thus
len p = ((G .size()) - (H .size())) + 1
by A2, FINSEQ_1:40;
for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) )
let n be
Element of
dom p;
( n <= (len p) - 1 implies ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) )
( 1
<= n &
n <= len p )
by FINSEQ_3:25;
then
( 1
<= n &
n <= 1 )
by FINSEQ_1:40;
then A4:
n = 1
by XXREAL_0:1;
assume
n <= (len p) - 1
;
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) )
then
n <= 1
- 1
by FINSEQ_1:40;
hence
ex
v1,
v2 being
Vertex of
G ex
e being
object st
(
p . (n + 1) is
addEdge of
p . n,
v1,
e,
v2 &
e in (the_Edges_of G) \ (the_Edges_of (p . n)) &
v1 in the_Vertices_of (p . n) &
v2 in the_Vertices_of (p . n) )
by A4;
verum
end;
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
let H be
spanning Subgraph of
G;
( (G .size()) - (H .size()) = k + 1 implies ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) )
assume A7:
(G .size()) - (H .size()) = k + 1
;
ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
A8:
(the_Edges_of G) \ (the_Edges_of H) <> {}
set e0 = the
Element of
(the_Edges_of G) \ (the_Edges_of H);
A10:
the
Element of
(the_Edges_of G) \ (the_Edges_of H) in the_Edges_of G
by A8, TARSKI:def 3;
then reconsider e0 = the
Element of
(the_Edges_of G) \ (the_Edges_of H) as
Element of
the_Edges_of G ;
set u =
(the_Source_of G) . e0;
set w =
(the_Target_of G) . e0;
reconsider u =
(the_Source_of G) . e0,
w =
(the_Target_of G) . e0 as
Vertex of
G by A10, FUNCT_2:5;
A11:
the_Vertices_of G = the_Vertices_of H
by GLIB_000:def 33;
set H1 = the
addEdge of
H,
u,
e0,
w;
A12:
not
e0 in the_Edges_of H
by A8, XBOOLE_0:def 5;
A13:
k =
(G .size()) - ((H .size()) + 1)
by A7
.=
(G .size()) - ( the addEdge of H,u,e0,w .size())
by A12, A11, GLIB_006:111
;
A14:
the_Vertices_of the
addEdge of
H,
u,
e0,
w = the_Vertices_of H
by A11, GLIB_006:102;
the
addEdge of
H,
u,
e0,
w is
Subgraph of
G
proof
for
e being
object st
e in the_Edges_of the
addEdge of
H,
u,
e0,
w holds
e in the_Edges_of G
proof
let e be
object ;
( e in the_Edges_of the addEdge of H,u,e0,w implies e in the_Edges_of G )
assume A15:
e in the_Edges_of the
addEdge of
H,
u,
e0,
w
;
e in the_Edges_of G
the_Edges_of the
addEdge of
H,
u,
e0,
w = (the_Edges_of H) \/ {e0}
by A11, A12, GLIB_006:def 11;
end;
then A16:
the_Edges_of the
addEdge of
H,
u,
e0,
w c= the_Edges_of G
by TARSKI:def 3;
now for e being set st e in the_Edges_of the addEdge of H,u,e0,w holds
( (the_Source_of the addEdge of H,u,e0,w) . e = (the_Source_of G) . e & (the_Target_of the addEdge of H,u,e0,w) . e = (the_Target_of G) . e )let e be
set ;
( e in the_Edges_of the addEdge of H,u,e0,w implies ( (the_Source_of the addEdge of H,u,e0,w) . b1 = (the_Source_of G) . b1 & (the_Target_of the addEdge of H,u,e0,w) . b1 = (the_Target_of G) . b1 ) )assume
e in the_Edges_of the
addEdge of
H,
u,
e0,
w
;
( (the_Source_of the addEdge of H,u,e0,w) . b1 = (the_Source_of G) . b1 & (the_Target_of the addEdge of H,u,e0,w) . b1 = (the_Target_of G) . b1 )then A17:
e in (the_Edges_of H) \/ {e0}
by A11, A12, GLIB_006:def 11;
per cases
( e <> e0 or e = e0 )
;
suppose
e <> e0
;
( (the_Source_of the addEdge of H,u,e0,w) . b1 = (the_Source_of G) . b1 & (the_Target_of the addEdge of H,u,e0,w) . b1 = (the_Target_of G) . b1 )then
not
e in {e0}
by TARSKI:def 1;
then A18:
e in the_Edges_of H
by A17, XBOOLE_0:def 3;
thus (the_Source_of the addEdge of H,u,e0,w) . e =
(the_Source_of H) . e
by A18, GLIB_006:def 9
.=
(the_Source_of G) . e
by A18, GLIB_000:def 32
;
(the_Target_of the addEdge of H,u,e0,w) . e = (the_Target_of G) . ethus (the_Target_of the addEdge of H,u,e0,w) . e =
(the_Target_of H) . e
by A18, GLIB_006:def 9
.=
(the_Target_of G) . e
by A18, GLIB_000:def 32
;
verum end; suppose A19:
e = e0
;
( (the_Source_of the addEdge of H,u,e0,w) . b1 = (the_Source_of G) . b1 & (the_Target_of the addEdge of H,u,e0,w) . b1 = (the_Target_of G) . b1 )then
e DJoins u,
w, the
addEdge of
H,
u,
e0,
w
by A11, A12, GLIB_006:105;
hence
(
(the_Source_of the addEdge of H,u,e0,w) . e = (the_Source_of G) . e &
(the_Target_of the addEdge of H,u,e0,w) . e = (the_Target_of G) . e )
by A19, GLIB_000:def 14;
verum end; end;
hence
the
addEdge of
H,
u,
e0,
w is
Subgraph of
G
by A14, A16, GLIB_000:def 32;
verum
end;
then
the
addEdge of
H,
u,
e0,
w is
spanning Subgraph of
G
by A11, A14, GLIB_000:def 33;
then consider p being non
empty Graph-yielding _finite FinSequence such that A20:
(
p . 1
== the
addEdge of
H,
u,
e0,
w &
p . (len p) = G &
len p = ((G .size()) - ( the addEdge of H,u,e0,w .size())) + 1 )
and A21:
for
n being
Element of
dom p st
n <= (len p) - 1 holds
ex
v1,
v2 being
Vertex of
G ex
e being
object st
(
p . (n + 1) is
addEdge of
p . n,
v1,
e,
v2 &
e in (the_Edges_of G) \ (the_Edges_of (p . n)) &
v1 in the_Vertices_of (p . n) &
v2 in the_Vertices_of (p . n) )
by A6, A13;
reconsider q =
<*H*> ^ p as non
empty Graph-yielding _finite FinSequence ;
take
q
;
( q . 1 == H & q . (len q) = G & len q = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) ) )
A22:
q . 1
= H
by FINSEQ_1:41;
thus
q . 1
== H
by FINSEQ_1:41;
( q . (len q) = G & len q = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) ) )
A23:
len q =
(len <*H*>) + (len p)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:40
;
len p in dom p
by FINSEQ_5:6;
hence
q . (len q) = G
by A20, A23, FINSEQ_3:103;
( len q = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) ) )
A24:
((H .size()) + 1) - 1
= ( the addEdge of H,u,e0,w .size()) - 1
by A12, A11, GLIB_006:111;
thus
len q = ((G .size()) - (H .size())) + 1
by A20, A23, A24;
for n being Element of dom q st n <= (len q) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )
let n be
Element of
dom q;
( n <= (len q) - 1 implies ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) )
assume
n <= (len q) - 1
;
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )
per cases then
( n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )
by Lm13;
suppose A25:
n = 1
;
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )take
u
;
ex v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,u,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & u in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )take
w
;
ex e being object st
( q . (n + 1) is addEdge of q . n,u,e,w & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & u in the_Vertices_of (q . n) & w in the_Vertices_of (q . n) )take
e0
;
( q . (n + 1) is addEdge of q . n,u,e0,w & e0 in (the_Edges_of G) \ (the_Edges_of (q . n)) & u in the_Vertices_of (q . n) & w in the_Vertices_of (q . n) )
1
in dom p
by FINSEQ_5:6;
then A26:
p . 1 =
q . ((len <*H*>) + 1)
by FINSEQ_1:def 7
.=
q . (n + 1)
by A25, FINSEQ_1:40
;
the
addEdge of
H,
u,
e0,
w is
addEdge of
q . n,
u,
e0,
w
by A25, FINSEQ_1:41;
hence
q . (n + 1) is
addEdge of
q . n,
u,
e0,
w
by A26, A20, GLIB_006:101;
( e0 in (the_Edges_of G) \ (the_Edges_of (q . n)) & u in the_Vertices_of (q . n) & w in the_Vertices_of (q . n) )thus
e0 in (the_Edges_of G) \ (the_Edges_of (q . n))
by A10, A12, A22, A25, XBOOLE_0:def 5;
( u in the_Vertices_of (q . n) & w in the_Vertices_of (q . n) )thus
(
u in the_Vertices_of (q . n) &
w in the_Vertices_of (q . n) )
by A11, A22, A25;
verum end; suppose A27:
(
n - 1
in dom p &
n - 1
<= (len p) - 1 )
;
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )then reconsider m =
n - 1 as
Element of
dom p ;
consider v1,
v2 being
Vertex of
G,
e being
object such that A28:
p . (m + 1) is
addEdge of
p . m,
v1,
e,
v2
and A29:
(
e in (the_Edges_of G) \ (the_Edges_of (p . m)) &
v1 in the_Vertices_of (p . m) &
v2 in the_Vertices_of (p . m) )
by A21, A27;
take
v1
;
ex v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )take
v2
;
ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )take
e
;
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) )A30:
1
<= n
by FINSEQ_3:25;
n <= len p
by A27, XREAL_1:9;
then
n in dom p
by A30, FINSEQ_3:25;
then A31:
p . n =
q . ((len <*H*>) + n)
by FINSEQ_1:def 7
.=
q . (n + 1)
by FINSEQ_1:40
;
p . m =
q . ((len <*H*>) + m)
by FINSEQ_1:def 7
.=
q . (m + 1)
by FINSEQ_1:40
.=
q . n
;
hence
(
q . (n + 1) is
addEdge of
q . n,
v1,
e,
v2 &
e in (the_Edges_of G) \ (the_Edges_of (q . n)) &
v1 in the_Vertices_of (q . n) &
v2 in the_Vertices_of (q . n) )
by A28, A29, A31;
verum end;
end;
A32:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A5);
let H be spanning Subgraph of G; ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
(G .size()) - (H .size()) is Nat
by GLIB_000:75, NAT_1:21;
hence
ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
by A32; verum