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 Tree-like
set PCS = PRIM:CompSeq G1;
defpred S₁[ Nat] means for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . $1) `1 ,((PRIM:CompSeq G1) . $1) `2 holds G2 is Tree-like ;
set G0 = (PRIM:CompSeq G1) . 0 ;
set src = choose (the_Vertices_of G1);

now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (PRIM:CompSeq G1) . n;
set Gn1 = (PRIM:CompSeq G1) . (n + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G1) . n);
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n));
consider G3 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 ;
A1: (PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n) by Def17;
A2: ((PRIM:CompSeq G1) . n) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1 ) by Th30;
((PRIM:CompSeq G1) . n) `1 is non empty Subset of (the_Vertices_of G1) by Th30;
then A3: ( the_Vertices_of G3 = ((PRIM:CompSeq G1) . n) `1 & the_Edges_of G3 = ((PRIM:CompSeq G1) . n) `2 ) by A2, GLIB_000:def 39;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
then A5: G3 is Tree-like ;

now

A6: G3 .order() = (G3 .size() ) + 1 by A5, GLIB_002:46;
let G2 be inducedSubgraph of G1,((PRIM:CompSeq G1) . (n + 1)) `1 ,((PRIM:CompSeq G1) . (n + 1)) `2 ; :: thesis: G2 is Tree-like
A7: ((PRIM:CompSeq G1) . (n + 1)) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . (n + 1)) `1 ) by Th30;
((PRIM:CompSeq G1) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G1) by Th30;
then A8: the_Vertices_of G2 = ((PRIM:CompSeq G1) . (n + 1)) `1 by A7, GLIB_000:def 39;

now

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} ) ;

suppose PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} ; :: thesis: G2 is Tree-like

then (PRIM:CompSeq G1) . n = (PRIM:CompSeq G1) . (n + 1) by A1, Def15;
hence G2 is Tree-like by A4; :: thesis: verum

end;

suppose A9: PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} ; :: thesis: G2 is Tree-like

set GnV = ((PRIM:CompSeq G1) . n) `1 ;
set GnVg = (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 );
A10: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ),G1 by A9, Def13;

A11: now

assume A12: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in ((PRIM:CompSeq G1) . n) `2 ; :: thesis: contradiction
then (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 by A2, GLIB_000:34;
then A13: not (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ) by XBOOLE_0:def 5;
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 by A2, A12, GLIB_000:34;
then not (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ) by XBOOLE_0:def 5;
hence contradiction by A10, A13, GLIB_000:def 17; :: thesis: verum

end;

consider v being Vertex of G1 such that
A14: not v in ((PRIM:CompSeq G1) . n) `1 and
A15: (PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {v}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})] by A1, A9, Th28;
A16: card (((PRIM:CompSeq G1) . (n + 1)) `1 ) = card ((((PRIM:CompSeq G1) . n) `1 ) \/ {v}) by A15, MCART_1:7
.= (card (((PRIM:CompSeq G1) . n) `1 )) + 1 by A14, CARD_2:54 ;
card (((PRIM:CompSeq G1) . (n + 1)) `2 ) = card ((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}) by A15, MCART_1:7
.= (card (((PRIM:CompSeq G1) . n) `2 )) + 1 by A11, CARD_2:54 ;
then G2 .order() = (G2 .size() ) + 1 by A3, A7, A8, A6, A16, GLIB_000:def 39;
hence G2 is Tree-like by GLIB_002:47; :: thesis: verum

end;

end;

end;

hence G2 is Tree-like ; :: thesis: verum

end;

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

end;

then A17: for n being Nat st S₁[n] holds
S₁[n + 1] ;
(PRIM:CompSeq G1) . 0 = PRIM:Init G1 by Def17;
then ( ((PRIM:CompSeq G1) . 0 ) `1 = {(choose (the_Vertices_of G1))} & ((PRIM:CompSeq G1) . 0 ) `2 = {} ) by MCART_1:7;
then A18: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A17);
hence for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is Tree-like ; :: thesis: verum