defpred S₁[ Nat] means for G being _finite simple _Graph
for W being set
for H being inducedSubgraph of G,W st (G .order()) - (H .order()) = $1 holds
ex p being non empty Graph-yielding _finite simple FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) );
A1: S₁[ 0 ]

proof

let G be _finite simple _Graph; :: thesis:
let W be set ; :: thesis:
let H be inducedSubgraph of G,W; :: thesis:
assume A2: (G .order()) - (H .order()) = 0 ; :: thesis:
then H is spanning by GLIB_000:117;
then A3: G == H by GLIB_000:120;
set p = <*G*>;
take <*G*> ; :: thesis:
thus <*G*> . 1 == H by A3; :: thesis:
thus <*G*> . (len <*G*>) = <*G*> . 1 by FINSEQ_1:40
.= G ; :: thesis:
thus len <*G*> = ((G .order()) - (H .order())) + 1 by A2, FINSEQ_1:40; :: thesis:
let n be Element of dom <*G*>; :: thesis:
( 1 <= n & n <= len <*G*> ) by FINSEQ_3:25;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= (len <*G*>) - 1 ; :: thesis:
then n <= 1 - 1 by FINSEQ_1:40;
hence ex v being object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) by A4; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
let G be _finite simple _Graph; :: thesis:
let W be set ; :: thesis:
let H be inducedSubgraph of G,W; :: thesis:
assume A7: (G .order()) - (H .order()) = k + 1 ; :: thesis:
A8: (the_Vertices_of G) \ (the_Vertices_of H) <> {}

proof

assume (the_Vertices_of G) \ (the_Vertices_of H) = {} ; :: thesis:
then the_Vertices_of G c= the_Vertices_of H by XBOOLE_1:37;
then A9: the_Vertices_of G = the_Vertices_of H by XBOOLE_0:def 10;
G .order() = card (the_Vertices_of G) by GLIB_000:def 24
.= H .order() by A9, GLIB_000:def 24 ;
then 0 = k + 1 by A7;
hence contradiction ; :: thesis:

end;

set v0 = the Element of (the_Vertices_of G) \ (the_Vertices_of H);
the Element of (the_Vertices_of G) \ (the_Vertices_of H) in (the_Vertices_of G) \ (the_Vertices_of H) by A8;
then reconsider v0 = the Element of (the_Vertices_of G) \ (the_Vertices_of H) as Vertex of G ;
set G2 = the removeVertex of G,v0;
A10: the_Vertices_of G <> the_Vertices_of H by A8, XBOOLE_1:37;
then A11: not G is _trivial by GLIB_000:121, GLIB_000:def 33;
then A12: ( the removeVertex of G,v0 .order()) + 1 = G .order() by GLIB_000:48;
then A13: ( the removeVertex of G,v0 .order()) - (H .order()) = k by A7;
A14: the_Edges_of the removeVertex of G,v0 = G .edgesBetween ((the_Vertices_of G) \ {v0}) by A11, GLIB_000:47
.= (G .edgesBetween (the_Vertices_of G)) \ (v0 .edgesInOut()) by GLIB_000:107
.= (the_Edges_of G) \ (v0 .edgesInOut()) by GLIB_000:34 ;
( the_Vertices_of H c= the_Vertices_of the removeVertex of G,v0 & the_Edges_of H c= the_Edges_of the removeVertex of G,v0 )

proof

A15: not v0 in the_Vertices_of H by A8, XBOOLE_0:def 5;
the_Vertices_of H c= (the_Vertices_of G) \ {v0} by A15, ZFMISC_1:34;
hence the_Vertices_of H c= the_Vertices_of the removeVertex of G,v0 by A11, GLIB_000:47; :: thesis:
(the_Edges_of H) /\ (v0 .edgesInOut()) = {}

proof

assume A16: (the_Edges_of H) /\ (v0 .edgesInOut()) <> {} ; :: thesis:
set e = the Element of (the_Edges_of H) /\ (v0 .edgesInOut());
A17: ( the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) in the_Edges_of H & the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) in v0 .edgesInOut() ) by A16, XBOOLE_0:def 4;

per cases ) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 or (the_Target_of G) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 ) by GLIB_000:61;

suppose (the_Source_of G) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 ; :: thesis:

then (the_Source_of H) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 by A17, GLIB_000:def 32;
hence contradiction by A15, A17, FUNCT_2:5; :: thesis:

end;

suppose (the_Target_of G) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 ; :: thesis:

then (the_Target_of H) . the Element of (the_Edges_of H) /\ (v0 .edgesInOut()) = v0 by A17, GLIB_000:def 32;
hence contradiction by A15, A17, FUNCT_2:5; :: thesis:

end;

then the_Edges_of H = (the_Edges_of H) \ (v0 .edgesInOut()) by XBOOLE_0:def 7, XBOOLE_1:83;
hence the_Edges_of H c= the_Edges_of the removeVertex of G,v0 by A14, XBOOLE_1:33; :: thesis:

end;

then A18: H is Subgraph of the removeVertex of G,v0 by GLIB_000:44;
H is inducedSubgraph of the removeVertex of G,v0,W

proof

H != G by A10, GLIB_000:def 34;
then W is non empty Subset of (the_Vertices_of G) by GLIB_000:def 37;
then A19: ( the_Vertices_of H = W & the_Edges_of H = G .edgesBetween W ) by GLIB_000:def 37;
then A20: W is non empty Subset of (the_Vertices_of the removeVertex of G,v0) by A18, GLIB_000:def 32;
for x being object st x in G .edgesBetween W holds
x in the removeVertex of G,v0 .edgesBetween W

proof

let x be object ; :: thesis:
assume A21: x in G .edgesBetween W ; :: thesis:
reconsider e = x as set by TARSKI:1;
A22: ( (the_Source_of G) . e in W & (the_Target_of G) . e in W ) by A21, GLIB_000:31;
A23: e in the_Edges_of the removeVertex of G,v0

proof

assume not e in the_Edges_of the removeVertex of G,v0 ; :: thesis:
then e in v0 .edgesInOut() by A14, A21, XBOOLE_0:def 5;

per cases ) . e = v0 or (the_Target_of G) . e = v0 ) by GLIB_000:61;

suppose (the_Source_of G) . e = v0 ; :: thesis:

hence contradiction by A8, A19, A22, XBOOLE_0:def 5; :: thesis:

end;

suppose (the_Target_of G) . e = v0 ; :: thesis:

hence contradiction by A8, A19, A22, XBOOLE_0:def 5; :: thesis:

end;

then ( (the_Source_of the removeVertex of G,v0) . e = (the_Source_of G) . e & (the_Target_of the removeVertex of G,v0) . e = (the_Target_of G) . e ) by GLIB_000:def 32;
hence x in the removeVertex of G,v0 .edgesBetween W by A22, A23, GLIB_000:31; :: thesis:

end;

then A24: G .edgesBetween W c= the removeVertex of G,v0 .edgesBetween W by TARSKI:def 3;
the removeVertex of G,v0 .edgesBetween W c= G .edgesBetween W by GLIB_000:76;
then the removeVertex of G,v0 .edgesBetween W = the_Edges_of H by A19, A24, XBOOLE_0:def 10;
hence H is inducedSubgraph of the removeVertex of G,v0,W by A18, A19, A20, GLIB_000:def 37; :: thesis:

end;

then consider p being non empty Graph-yielding _finite simple FinSequence such that
A25: ( p . 1 == H & p . (len p) = the removeVertex of G,v0 & len p = (( the removeVertex of G,v0 .order()) - (H .order())) + 1 ) and
A26: for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being finite set st
( v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) by A6, A13;
set q = p ^ <*G*>;
take p ^ <*G*> ; :: thesis:
1 in dom p by FINSEQ_5:6;
hence (p ^ <*G*>) . 1 == H by A25, FINSEQ_1:def 7; :: thesis:
A27: len (p ^ <*G*>) = (len p) + (len <*G*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A28: (p ^ <*G*>) . (len (p ^ <*G*>)) = G by FINSEQ_1:42; :: thesis:
thus len (p ^ <*G*>) = ((G .order()) - (H .order())) + 1 by A12, A25, A27; :: thesis:
let n be Element of dom (p ^ <*G*>); :: thesis:
assume n <= (len (p ^ <*G*>)) - 1 ; :: thesis:

per cases by Lm12;

suppose A29: n = (len (p ^ <*G*>)) - 1 ; :: thesis:

then A30: (p ^ <*G*>) . (n + 1) = G by A28;
A31: 1 <= n by FINSEQ_3:25;
A32: n = len p by A27, A29;
then n in dom p by A31, FINSEQ_3:25;
then A33: (p ^ <*G*>) . n = the removeVertex of G,v0 by A25, A32, FINSEQ_1:def 7;
reconsider V = v0 .allNeighbors() as finite set ;
take v0 ; :: thesis:
take V ; :: thesis:
v0 in {v0} by TARSKI:def 1;
then not v0 in (the_Vertices_of G) \ {v0} by XBOOLE_0:def 5;
then not v0 in the_Vertices_of the removeVertex of G,v0 by A11, GLIB_000:47;
hence v0 in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) by A33, XBOOLE_0:def 5; :: thesis:
for x being object st x in V holds
x in the_Vertices_of the removeVertex of G,v0

proof

let x be object ; :: thesis:
assume A34: x in V ; :: thesis:
then x <> v0 by GLIB_000:112;
then A35: not x in {v0} by TARSKI:def 1;
x in (the_Vertices_of G) \ {v0} by A34, A35, XBOOLE_0:def 5;
hence x in the_Vertices_of the removeVertex of G,v0 by A11, GLIB_000:47; :: thesis:

end;

hence V c= the_Vertices_of ((p ^ <*G*>) . n) by A33, TARSKI:def 3; :: thesis:
thus (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,V by A11, A30, A33, Th47; :: thesis:

end;

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

then A37: 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 A37, FINSEQ_3:25;
consider v being object , V being finite set such that
A38: ( v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) & V c= the_Vertices_of (p . m) & p . (m + 1) is addAdjVertexAll of p . m,v,V ) by A26, A36;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A36, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A39: (p ^ <*G*>) . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A40: (p ^ <*G*>) . n = p . m by FINSEQ_1:def 7;
take v ; :: thesis:
take V ; :: thesis:
(the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) c= (the_Vertices_of G) \ (the_Vertices_of (p . m)) by XBOOLE_1:33;
hence v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) by A38, A40; :: thesis:
thus ( V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) by A38, A39, A40; :: thesis:

end;

A41: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
let G be _finite simple _Graph; :: thesis:
let W be set ; :: thesis:
let H be inducedSubgraph of G,W; :: thesis:
(G .order()) - (H .order()) is Nat by GLIB_000:75, NAT_1:21;
hence ex p being non empty Graph-yielding _finite simple FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) ) by A41; :: thesis: