let G be _finite _Graph; :: thesis: 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 S₁[ 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: S₁[ 0 ]

proof

let H be spanning Subgraph of G; :: thesis: ( (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 ; :: thesis: 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 GLIB_000:119;
reconsider p = <*G*> as non empty Graph-yielding _finite FinSequence ;
take p ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let H be spanning Subgraph of G; :: thesis: ( (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 ; :: thesis: 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) <> {}

proof

assume A9: (the_Edges_of G) \ (the_Edges_of H) = {} ; :: thesis: contradiction
0 = card ((the_Edges_of G) \ (the_Edges_of H)) by A9
.= (card (the_Edges_of G)) - (card (the_Edges_of H)) by CARD_2:44
.= (G .size()) - (card (the_Edges_of H)) by GLIB_000:def 25
.= (G .size()) - (H .size()) by GLIB_000:def 25 ;
hence contradiction by A7; :: thesis: verum

end;

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 ; :: thesis: ( 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 ; :: thesis: 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;

per cases then ( e in the_Edges_of H or e in {e0} ) by A15, XBOOLE_0:def 3;

suppose e in the_Edges_of H ; :: thesis: e in the_Edges_of G

hence e in the_Edges_of G ; :: thesis: verum

end;

suppose e in {e0} ; :: thesis: e in the_Edges_of G

hence e in the_Edges_of G by A10, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A16: the_Edges_of the addEdge of H,u,e0,w c= the_Edges_of G by TARSKI:def 3;

now :: thesis: 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 ; :: thesis: ( e in the_Edges_of the addEdge of H,u,e0,w implies ( (the_Source_of the addEdge of H,u,e0,w) . b₁ = (the_Source_of G) . b₁ & (the_Target_of the addEdge of H,u,e0,w) . b₁ = (the_Target_of G) . b₁ ) )
assume e in the_Edges_of the addEdge of H,u,e0,w ; :: thesis: ( (the_Source_of the addEdge of H,u,e0,w) . b₁ = (the_Source_of G) . b₁ & (the_Target_of the addEdge of H,u,e0,w) . b₁ = (the_Target_of G) . b₁ )
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 ; :: thesis: ( (the_Source_of the addEdge of H,u,e0,w) . b₁ = (the_Source_of G) . b₁ & (the_Target_of the addEdge of H,u,e0,w) . b₁ = (the_Target_of G) . b₁ )

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 ; :: thesis: (the_Target_of the addEdge of H,u,e0,w) . e = (the_Target_of G) . e
thus (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 ; :: thesis: verum

end;

suppose A19: e = e0 ; :: thesis: ( (the_Source_of the addEdge of H,u,e0,w) . b₁ = (the_Source_of G) . b₁ & (the_Target_of the addEdge of H,u,e0,w) . b₁ = (the_Target_of G) . b₁ )

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; :: thesis: verum

end;

end;

end;

hence the addEdge of H,u,e0,w is Subgraph of G by A14, A16, GLIB_000:def 32; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: verum

end;

suppose A27: ( n - 1 in dom p & n - 1 <= (len p) - 1 ) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

end;

end;

end;

A32: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
let H be spanning Subgraph of G; :: thesis: 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; :: thesis: verum