let G1 be finite real-weighted WGraph; :: thesis: for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is connected
defpred S₁[ Nat] means for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . $1) `1 ,((PRIM:CompSeq G1) . $1) `2 holds G2 is connected ;
set G0 = (PRIM:CompSeq G1) . 0 ;
set v = choose (the_Vertices_of G1);

now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A1: S₁[n] ; :: thesis: S₁[n + 1]
set Gn = (PRIM:CompSeq G1) . n;
set Gn1 = (PRIM:CompSeq G1) . (n + 1);
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n));
set v1 = (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)));
set v2 = (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)));
A2: (PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n) by Def17;

now

let Gn1s be inducedSubgraph of G1,((PRIM:CompSeq G1) . (n + 1)) `1 ,((PRIM:CompSeq G1) . (n + 1)) `2 ; :: thesis: Gn1s is connected
A3: ( ((PRIM:CompSeq G1) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G1) & ((PRIM:CompSeq G1) . (n + 1)) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . (n + 1)) `1 ) ) by Th30;
then A4: the_Vertices_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `1 by GLIB_000:def 39;
A5: the_Edges_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `2 by A3, GLIB_000:def 39;

now

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} or ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) or ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & not (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) ) ;

suppose PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} ; :: thesis: Gn1s is connected

then (PRIM:CompSeq G1) . (n + 1) = (PRIM:CompSeq G1) . n by A2, Def15;
hence Gn1s is connected by A1; :: thesis: verum

end;

suppose A6: ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) ; :: thesis: Gn1s is connected

then A7: (PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {((the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))))}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})] by A2, Def15;
then A8: ((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))} by MCART_1:7;
A9: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) by A6;
then reconsider v1 = (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as Vertex of G1 by FUNCT_2:7;
A10: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),v1,G1 by A9, GLIB_000:def 15;
consider Gns being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 ;
A11: Gns is connected by A1;
A12: ( ((PRIM:CompSeq G1) . n) `1 is non empty Subset of (the_Vertices_of G1) & ((PRIM:CompSeq G1) . n) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1 ) ) by Th30;
then A13: the_Vertices_of Gns = ((PRIM:CompSeq G1) . n) `1 by GLIB_000:def 39;
A14: ((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1 ) \/ {v1} by A7, MCART_1:7;
then A15: the_Vertices_of Gns c= the_Vertices_of Gn1s by A4, A13, XBOOLE_1:7;
the_Edges_of Gns = ((PRIM:CompSeq G1) . n) `2 by A12, GLIB_000:def 39;
then reconsider Gns = Gns as Subgraph of Gn1s by A5, A8, A15, GLIB_000:47, XBOOLE_1:7;
consider src being Vertex of Gns;
reconsider src9 = src as Vertex of Gn1s by GLIB_000:45;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))} by TARSKI:def 1;
then choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of Gn1s by A5, A8, XBOOLE_0:def 3;
then A16: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),v1,Gn1s by A10, GLIB_000:76;

now

let x be Vertex of Gn1s; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

now

per cases ( x = v1 or x <> v1 ) ;

suppose A17: x = v1 ; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

reconsider v29 = (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as Vertex of Gns by A6, A12, GLIB_000:def 39;
consider W being Walk of Gns such that
A18: W is_Walk_from src,v29 by A11, GLIB_002:def 1;
reconsider W = W as Walk of Gn1s by GLIB_001:168;
W is_Walk_from src9,(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) by A18, GLIB_001:20;
then W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src9,x by A16, A17, GLIB_001:67;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

suppose x <> v1 ; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

then not x in {v1} by TARSKI:def 1;
then reconsider x9 = x as Vertex of Gns by A4, A14, A13, XBOOLE_0:def 3;
consider W being Walk of Gns such that
A19: W is_Walk_from src,x9 by A11, GLIB_002:def 1;
reconsider W9 = W as Walk of Gn1s by GLIB_001:168;
W9 is_Walk_from src9,x by A19, GLIB_001:20;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

end;

end;

hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

hence Gn1s is connected by GLIB_002:6; :: thesis: verum

end;

suppose A20: ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & not (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) ; :: thesis: Gn1s is connected

then A21: (PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {((the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))))}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})] by A2, Def15;
then A22: ((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))} by MCART_1:7;
A23: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ),G1 by A20, Def13;
then A24: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of G1 by GLIB_000:def 17;
then reconsider v2 = (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as Vertex of G1 by FUNCT_2:7;
A25: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),v2,G1 by A24, GLIB_000:def 15;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))} by TARSKI:def 1;
then choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of Gn1s by A5, A22, XBOOLE_0:def 3;
then A26: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),v2,Gn1s by A25, GLIB_000:76;
consider Gns being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 ;
A27: Gns is connected by A1;
A28: ( ((PRIM:CompSeq G1) . n) `1 is non empty Subset of (the_Vertices_of G1) & ((PRIM:CompSeq G1) . n) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1 ) ) by Th30;
then A29: the_Vertices_of Gns = ((PRIM:CompSeq G1) . n) `1 by GLIB_000:def 39;
A30: ((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1 ) \/ {v2} by A21, MCART_1:7;
then A31: the_Vertices_of Gns c= the_Vertices_of Gn1s by A4, A29, XBOOLE_1:7;
the_Edges_of Gns = ((PRIM:CompSeq G1) . n) `2 by A28, GLIB_000:def 39;
then reconsider Gns = Gns as Subgraph of Gn1s by A5, A22, A31, GLIB_000:47, XBOOLE_1:7;
consider src being Vertex of Gns;
reconsider src9 = src as Vertex of Gn1s by GLIB_000:45;
A32: (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 by A20, A23, GLIB_000:def 17;

now

let x be Vertex of Gn1s; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

now

per cases ( x = v2 or x <> v2 ) ;

suppose A33: x = v2 ; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

reconsider v19 = (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as Vertex of Gns by A32, A28, GLIB_000:def 39;
consider W being Walk of Gns such that
A34: W is_Walk_from src,v19 by A27, GLIB_002:def 1;
reconsider W = W as Walk of Gn1s by GLIB_001:168;
W is_Walk_from src9,(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) by A34, GLIB_001:20;
then W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src9,x by A26, A33, GLIB_001:67;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

suppose x <> v2 ; :: thesis: ex W being Walk of Gn1s st W is_Walk_from src9,x

then not x in {v2} by TARSKI:def 1;
then reconsider x9 = x as Vertex of Gns by A4, A30, A29, XBOOLE_0:def 3;
consider W being Walk of Gns such that
A35: W is_Walk_from src,x9 by A27, GLIB_002:def 1;
reconsider W9 = W as Walk of Gn1s by GLIB_001:168;
W9 is_Walk_from src9,x by A35, GLIB_001:20;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

end;

end;

hence ex W being Walk of Gn1s st W is_Walk_from src9,x ; :: thesis: verum

end;

hence Gn1s is connected by GLIB_002:6; :: thesis: verum

end;

end;

end;

hence Gn1s is connected ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

then A36: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now

let G be inducedSubgraph of G1,((PRIM:CompSeq G1) . 0 ) `1 ,((PRIM:CompSeq G1) . 0 ) `2 ; :: thesis: G is connected
A37: (PRIM:CompSeq G1) . 0 = PRIM:Init G1 by Def17;
then ((PRIM:CompSeq G1) . 0 ) `1 = {(choose (the_Vertices_of G1))} by MCART_1:7;
then reconsider G9 = G as inducedSubgraph of G1,{(choose (the_Vertices_of G1))}, {} by A37, MCART_1:7;
G9 is connected ;
hence G is connected ; :: thesis: verum

end;

then A38: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A38, A36);
hence for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is connected ; :: thesis: verum