let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V1 be set ; :: thesis:
defpred S₁[ Nat] means for V2 being finite set
for G1 being addAdjVertexAll of G2,v,V1 \/ V2 st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 & V1 misses V2 & card V2 = $1 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V2) + 2 & p . 2 is addAdjVertexAll of G2,v,V1 & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) );
A1: S₁[ 0 ]

proof

let V2 be finite set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V1 \/ V2; :: thesis:
assume that
( V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( V1 misses V2 & card V2 = 0 ) ; :: thesis:
reconsider p = <*G2,G1*> as non empty Graph-yielding FinSequence ;
take p ; :: thesis:
thus p . 1 = G2 ; :: thesis:
thus p . (len p) = p . 2 by FINSEQ_1:44
.= G1 ; :: thesis:
thus len p = (card V2) + 2 by A2, FINSEQ_1:44; :: thesis:
V2 = {} by A2;
hence p . 2 is addAdjVertexAll of G2,v,V1 ; :: thesis:
let n be Element of dom p; :: thesis:
assume ( 2 <= n & n <= (len p) - 1 ) ; :: thesis:
then ( 2 <= n & n <= 2 - 1 ) by FINSEQ_1:44;
hence ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) by XXREAL_0:2; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
let V2 be finite set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V1 \/ V2; :: thesis:
assume that
A5: ( V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A6: ( V1 misses V2 & card V2 = k + 1 ) ; :: thesis:
set v0 = the Element of V2;
set V3 = V2 \ { the Element of V2};
A7: not V2 is empty by A6;
A8: V2 = (V2 \ { the Element of V2}) \/ { the Element of V2} by A7, ZFMISC_1:116;
V1 \/ (V2 \ { the Element of V2}) c= V1 \/ V2 by XBOOLE_1:9;
then A9: V1 \/ (V2 \ { the Element of V2}) c= the_Vertices_of G2 by A5, XBOOLE_1:1;
A10: V1 misses V2 \ { the Element of V2} by A6, XBOOLE_1:64;
the Element of V2 in { the Element of V2} by TARSKI:def 1;
then A11: not the Element of V2 in V2 \ { the Element of V2} by XBOOLE_0:def 5;
then A12: card V2 = (card (V2 \ { the Element of V2})) + 1 by A8, CARD_2:41;
then A13: card (V2 \ { the Element of V2}) = k by A6;
the Element of V2 in V1 \/ V2 by A7, XBOOLE_1:7, TARSKI:def 3;
then reconsider v0 = the Element of V2 as Vertex of G2 by A5;
V1 /\ V2 = {} by A6, XBOOLE_0:def 7;
then not v0 in V1 by A7, XBOOLE_0:def 4;
then A14: not v0 in V1 \/ (V2 \ { the Element of V2}) by A11, XBOOLE_0:def 3;
G1 is addAdjVertexAll of G2,v,(V1 \/ (V2 \ { the Element of V2})) \/ {v0} by A8, XBOOLE_1:4;
then consider G3 being addAdjVertexAll of G2,v,V1 \/ (V2 \ { the Element of V2}), e being object such that
A15: not e in the_Edges_of G3 and
A16: ( G1 is addEdge of G3,v,e,v0 or G1 is addEdge of G3,v0,e,v ) by A5, A9, A14, Lm9;
consider p being non empty Graph-yielding FinSequence such that
A17: ( p . 1 = G2 & p . (len p) = G3 & len p = (card (V2 \ { the Element of V2})) + 2 & p . 2 is addAdjVertexAll of G2,v,V1 ) and
A18: for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G3) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) by A4, A5, A9, A10, A13;
reconsider q = p ^ <*G1*> as non empty Graph-yielding FinSequence ;
take q ; :: thesis:
1 in dom p by FINSEQ_5:6;
hence q . 1 = G2 by A17, FINSEQ_1:def 7; :: thesis:
A19: len q = (len p) + (len <*G1*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A20: q . (len q) = G1 by FINSEQ_1:42; :: thesis:
thus len q = (card V2) + 2 by A12, A17, A19; :: thesis:
(2 + (card (V2 \ { the Element of V2}))) - (card (V2 \ { the Element of V2})) <= (len p) - 0 by A17, XREAL_1:13;
then 2 in dom p by FINSEQ_3:25;
hence q . 2 is addAdjVertexAll of G2,v,V1 by A17, FINSEQ_1:def 7; :: thesis:
let n be Element of dom q; :: thesis:
assume A21: ( 2 <= n & n <= (len q) - 1 ) ; :: thesis:

per cases by Lm12;

suppose A22: n = (len q) - 1 ; :: thesis:

then A23: q . (n + 1) = G1 by A20;
1 <= n by FINSEQ_3:25;
then n in dom p by A19, A22, FINSEQ_3:25;
then A26: q . n = G3 by A17, A19, A22, FINSEQ_1:def 7;
( v0 in the_Vertices_of G3 & v in the_Vertices_of G3 )

proof

A27: v0 in the_Vertices_of G2 ;
the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_006:def 9;
hence v0 in the_Vertices_of G3 by A27; :: thesis:
v is Vertex of G3 by A5, A9, GLIB_007:50;
hence v in the_Vertices_of G3 ; :: thesis:

end;

then ( e DJoins v,v0,G1 or e DJoins v0,v,G1 ) by A15, A16, GLIB_006:105;
then A28: e in the_Edges_of G1 by GLIB_000:def 14;
take v0 ; :: thesis:
take e ; :: thesis:
thus e in (the_Edges_of G1) \ (the_Edges_of (q . n)) by A15, A26, A28, XBOOLE_0:def 5; :: thesis:
thus ( q . (n + 1) is addEdge of q . n,v,e,v0 or q . (n + 1) is addEdge of q . n,v0,e,v ) by A16, A23, A26; :: thesis:

end;

suppose A29: n <= (len p) - 1 ; :: thesis:

then A30: n + 0 <= ((len p) - 1) + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A30, FINSEQ_3:25;
consider w being Vertex of G2, e being object such that
A31: ( e in (the_Edges_of G3) \ (the_Edges_of (p . m)) & ( p . (m + 1) is addEdge of p . m,v,e,w or p . (m + 1) is addEdge of p . m,w,e,v ) ) by A18, A21, A29;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A29, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A32: q . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A33: q . n = p . m by FINSEQ_1:def 7;
the_Edges_of G3 c= the_Edges_of G1 by A16, GLIB_006:def 9;
then A34: (the_Edges_of G3) \ (the_Edges_of (p . m)) c= (the_Edges_of G1) \ (the_Edges_of (p . m)) by XBOOLE_1:33;
take w ; :: thesis:
take e ; :: thesis:
thus ( e in (the_Edges_of G1) \ (the_Edges_of (q . n)) & ( q . (n + 1) is addEdge of q . n,v,e,w or q . (n + 1) is addEdge of q . n,w,e,v ) ) by A31, A32, A33, A34; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence for V2 being finite set
for G1 being addAdjVertexAll of G2,v,V1 \/ V2 st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 & V1 misses V2 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V2) + 2 & p . 2 is addAdjVertexAll of G2,v,V1 & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) ) ; :: thesis: