let G1 be _finite real-weighted WGraph; :: thesis:
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 = the Element of the_Vertices_of G1;

now :: thesis:

let n be Nat; :: thesis:
set Gn = (PRIM:CompSeq G1) . n;
set Gn1 = (PRIM:CompSeq G1) . (n + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G1) . n);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . n);
set G3 = the 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 the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `1 & the_Edges_of the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `2 ) by A2, GLIB_000:def 37;
assume A4: S₁[n] ; :: thesis:
then A5: the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 is Tree-like ;

now :: thesis:

A6: the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 .order() = ( the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 .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:
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 37;

now :: thesis:

per cases ;

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

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

end;

suppose A9: PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} ; :: thesis:

set GnV = ((PRIM:CompSeq G1) . n) `1 ;
set GnVg = (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1);
A10: the Element of 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 :: thesis:

assume A12: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) in ((PRIM:CompSeq G1) . n) `2 ; :: thesis:
then (the_Target_of G1) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) in ((PRIM:CompSeq G1) . n) `1 by A2, GLIB_000:31;
then A13: not (the_Target_of G1) . the Element of 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) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) in ((PRIM:CompSeq G1) . n) `1 by A2, A12, GLIB_000:31;
then not (the_Source_of G1) . the Element of 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; :: thesis:

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) \/ { the Element of 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
.= (card (((PRIM:CompSeq G1) . n) `1)) + 1 by A14, CARD_2:41 ;
card (((PRIM:CompSeq G1) . (n + 1)) `2) = card ((((PRIM:CompSeq G1) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)}) by A15
.= (card (((PRIM:CompSeq G1) . n) `2)) + 1 by A11, CARD_2:41 ;
then G2 .order() = (G2 .size()) + 1 by A3, A7, A8, A6, A16, GLIB_000:def 37;
hence G2 is Tree-like by GLIB_002:47; :: thesis:

end;

end;

end;

hence G2 is Tree-like ; :: thesis:

end;

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

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 = { the Element of the_Vertices_of G1} & ((PRIM:CompSeq G1) . 0) `2 = {} ) ;
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: