let G1 be finite connected real-weighted WGraph; :: thesis: for G2 being inducedWSubgraph of G1,(PRIM:MST G1) `1 ,(PRIM:MST G1) `2 holds G2 is minimumSpanningTree of G1
set PMST = PRIM:MST G1;
set VG1 = the_Vertices_of G1;
set EG1 = the_Edges_of G1;
set WG1 = the_Weight_of G1;
let G2 be inducedWSubgraph of G1,(PRIM:MST G1) `1 ,(PRIM:MST G1) `2 ; :: thesis: G2 is minimumSpanningTree of G1
set PCS = PRIM:CompSeq G1;
A2: (PRIM:MST G1) `1 = the_Vertices_of G1 by Lm18;
(PRIM:MST G1) `2 in bool (the_Edges_of G1) by MCART_1:10;
then (PRIM:MST G1) `2 c= the_Edges_of G1 ;
then A3: (PRIM:MST G1) `2 c= G1 .edgesBetween ((PRIM:MST G1) `1 ) by A2, GLIB_000:37;
(PRIM:MST G1) `1 c= the_Vertices_of G1 by Lm18;
then A4: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (PRIM:MST G1) `2 ) by A2, A3, GLIB_000:def 39;
then A5: ( G2 is Tree-like & G2 is spanning ) by Lm17, GLIB_000:def 35;
reconsider G2' = G2 as Tree-like _Graph by Lm17;

now

assume A6: G2 is not minimumSpanningTree of G1 ; :: thesis: contradiction
set X = { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } ;

now

let x be set ; :: thesis: ( x in { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } implies x in G1 .allWSubgraphs() )
assume x in { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } ; :: thesis: x in G1 .allWSubgraphs()
then consider G2 being Element of G1 .allWSubgraphs() such that
A7: ( x = G2 & G2 is minimumSpanningTree of G1 ) ;
thus x in G1 .allWSubgraphs() by A7; :: thesis: verum

end;

then reconsider X = { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } as finite Subset of (G1 .allWSubgraphs() ) by TARSKI:def 3;

now

consider M being minimumSpanningTree of G1;
set M' = M .strict WGraphSelectors ;
( M .strict WGraphSelectors == M & the_Weight_of (M .strict WGraphSelectors ) = the_Weight_of M ) by Lm2;
then reconsider M' = M .strict WGraphSelectors as minimumSpanningTree of G1 by Th36;
dom M' = WGraphSelectors by Lm3;
then M' in G1 .allWSubgraphs() by Def10;
then M' in X ;
hence X <> {} ; :: thesis: verum

end;

then reconsider X = X as non empty finite Subset of (G1 .allWSubgraphs() ) ;
defpred S₁[ finite _Graph, Nat] means ( not ((PRIM:CompSeq G1) . ($2 + 1)) `2 c= the_Edges_of $1 & ( for n being Nat st n <= $2 holds
((PRIM:CompSeq G1) . n) `2 c= the_Edges_of $1 ) );
defpred S₂[ finite _Graph, finite _Graph] means ( card ((the_Edges_of $1) /\ (the_Edges_of G2)) > card ((the_Edges_of $2) /\ (the_Edges_of G2)) or ( card ((the_Edges_of $1) /\ (the_Edges_of G2)) = card ((the_Edges_of $2) /\ (the_Edges_of G2)) & ( for k1, k2 being Nat st S₁[$1,k1] & S₁[$2,k2] holds
k1 >= k2 ) ) );

A8: now

let G be Element of X; :: thesis: ex k1 being Nat st S₁[G,k1]
G in X ;
then consider G' being Element of G1 .allWSubgraphs() such that
A9: ( G = G' & G' is minimumSpanningTree of G1 ) ;
reconsider G' = G as minimumSpanningTree of G1 by A9;
A10: the_Vertices_of G2 = the_Vertices_of G' by A4, GLIB_000:def 35;

A11: now

assume A12: the_Edges_of G2 = the_Edges_of G' ; :: thesis: contradiction
the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10
.= the_Weight_of G' by A12, GLIB_003:def 10 ;
hence contradiction by A6, A10, A12, Th36, GLIB_000:89; :: thesis: verum

end;

defpred S₃[ Nat] means not ((PRIM:CompSeq G1) . $1) `2 c= the_Edges_of G';

now

assume the_Edges_of G2 c= the_Edges_of G' ; :: thesis: contradiction
then the_Edges_of G2 c< the_Edges_of G' by A11, XBOOLE_0:def 8;
then (G2 .size() ) + 1 < (G' .size() ) + 1 by CARD_2:67, XREAL_1:10;
then A13: G2 .order() < (G' .size() ) + 1 by A5, GLIB_002:46;
G2 .order() = G' .order() by A4, GLIB_000:def 35;
hence contradiction by A13, GLIB_002:46; :: thesis: verum

end;

then A14: ex n being Nat st S₃[n] by A4;
consider k3 being Nat such that
A15: ( S₃[k3] & ( for n being Nat st S₃[n] holds
k3 <= n ) ) from NAT_1:sch 5(A14);

now

assume k3 = 0 ; :: thesis: contradiction
then A16: not (PRIM:Init G1) `2 c= the_Edges_of G' by A15, Def15;
(PRIM:Init G1) `2 = {} by MCART_1:7;
hence contradiction by A16, XBOOLE_1:2; :: thesis: verum

end;

then consider k2 being Nat such that
A17: k2 + 1 = k3 by NAT_1:6;
(k2 + 1) - 1 < k3 - 0 by A17, XREAL_1:17;
then A18: ((PRIM:CompSeq G1) . k2) `2 c= the_Edges_of G' by A15;

now

let n be Nat; :: thesis: ( n <= k2 implies ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of G' )
assume n <= k2 ; :: thesis: ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of G'
then ((PRIM:CompSeq G1) . n) `2 c= ((PRIM:CompSeq G1) . k2) `2 by Lm13;
hence ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of G' by A18, XBOOLE_1:1; :: thesis: verum

end;

hence ex k1 being Nat st S₁[G,k1] by A15, A17; :: thesis: verum

end;

A19: now

let G be Element of X; :: thesis: for k1, k2 being Nat st S₁[G,k1] & S₁[G,k2] holds
k1 = k2
let k1, k2 be Nat; :: thesis: ( S₁[G,k1] & S₁[G,k2] implies k1 = k2 )
assume ( S₁[G,k1] & S₁[G,k2] ) ; :: thesis: k1 = k2
then ( k1 + 1 > k2 & k2 + 1 > k1 ) ;
then ( k1 >= k2 & k2 >= k1 ) by NAT_1:13;
hence k1 = k2 by XXREAL_0:1; :: thesis: verum

end;

A21: ( X is finite & X <> {} & X c= X ) ;

now

let x, y be Element of X; :: thesis: ( S₂[x,y] or S₂[y,x] )
x in X ;
then consider x' being WSubgraph of G1 such that
A22: ( x' = x & dom x' = WGraphSelectors ) by Def10;
y in X ;
then consider y' being WSubgraph of G1 such that
A23: ( y' = y & dom y' = WGraphSelectors ) by Def10;
set CX = card ((the_Edges_of x') /\ (the_Edges_of G2));
set CY = card ((the_Edges_of y') /\ (the_Edges_of G2));

now

per cases ( card ((the_Edges_of x') /\ (the_Edges_of G2)) < card ((the_Edges_of y') /\ (the_Edges_of G2)) or card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of x') /\ (the_Edges_of G2)) or card ((the_Edges_of x') /\ (the_Edges_of G2)) > card ((the_Edges_of y') /\ (the_Edges_of G2)) ) by XXREAL_0:1;

suppose card ((the_Edges_of x') /\ (the_Edges_of G2)) < card ((the_Edges_of y') /\ (the_Edges_of G2)) ; :: thesis: ( S₂[x,y] or S₂[y,x] )

hence ( S₂[x,y] or S₂[y,x] ) by A22, A23; :: thesis: verum

end;

suppose A24: card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of x') /\ (the_Edges_of G2)) ; :: thesis: ( S₂[x,y] or S₂[y,x] )

consider k1 being Nat such that
A25: S₁[x,k1] by A8;
consider k2 being Nat such that
A26: S₁[y,k2] by A8;

now

per cases ( k1 >= k2 or k1 < k2 ) ;

suppose A27: k1 >= k2 ; :: thesis: ( S₂[x,y] or S₂[y,x] )

now

let z1, z2 be Nat; :: thesis: ( S₁[x,z1] & S₁[y,z2] implies z1 >= z2 )
assume ( S₁[x,z1] & S₁[y,z2] ) ; :: thesis: z1 >= z2
then ( z1 = k1 & z2 = k2 ) by A19, A25, A26;
hence z1 >= z2 by A27; :: thesis: verum

end;

hence ( S₂[x,y] or S₂[y,x] ) by A22, A23, A24; :: thesis: verum

end;

suppose A28: k1 < k2 ; :: thesis: ( S₂[x,y] or S₂[y,x] )

now

let z1, z2 be Nat; :: thesis: ( S₁[x,z1] & S₁[y,z2] implies z1 <= z2 )
assume ( S₁[x,z1] & S₁[y,z2] ) ; :: thesis: z1 <= z2
then ( z1 = k1 & z2 = k2 ) by A19, A25, A26;
hence z1 <= z2 by A28; :: thesis: verum

end;

hence ( S₂[x,y] or S₂[y,x] ) by A22, A23, A24; :: thesis: verum

end;

end;

end;

hence ( S₂[x,y] or S₂[y,x] ) ; :: thesis: verum

end;

suppose card ((the_Edges_of x') /\ (the_Edges_of G2)) > card ((the_Edges_of y') /\ (the_Edges_of G2)) ; :: thesis: ( S₂[x,y] or S₂[y,x] )

hence ( S₂[x,y] or S₂[y,x] ) by A22, A23; :: thesis: verum

end;

end;

end;

hence ( S₂[x,y] or S₂[y,x] ) ; :: thesis: verum

end;

then A29: for x, y being Element of X holds
( S₂[x,y] or S₂[y,x] ) ;

now

let x, y, z be Element of X; :: thesis: ( S₂[x,y] & S₂[y,z] implies S₂[x,z] )
assume A30: ( S₂[x,y] & S₂[y,z] ) ; :: thesis: S₂[x,z]
x in X ;
then consider x' being WSubgraph of G1 such that
A31: ( x' = x & dom x' = WGraphSelectors ) by Def10;
y in X ;
then consider y' being WSubgraph of G1 such that
A32: ( y' = y & dom y' = WGraphSelectors ) by Def10;
z in X ;
then consider z' being WSubgraph of G1 such that
A33: ( z' = z & dom z' = WGraphSelectors ) by Def10;
set CX = card ((the_Edges_of x') /\ (the_Edges_of G2));
set CY = card ((the_Edges_of y') /\ (the_Edges_of G2));
set CZ = card ((the_Edges_of z') /\ (the_Edges_of G2));

now

per cases ( card ((the_Edges_of x') /\ (the_Edges_of G2)) > card ((the_Edges_of y') /\ (the_Edges_of G2)) or ( card ((the_Edges_of x') /\ (the_Edges_of G2)) = card ((the_Edges_of y') /\ (the_Edges_of G2)) & ( for kx, ky being Nat st S₁[x',kx] & S₁[y',ky] holds
kx >= ky ) ) ) by A30, A31, A32;

suppose A34: card ((the_Edges_of x') /\ (the_Edges_of G2)) > card ((the_Edges_of y') /\ (the_Edges_of G2)) ; :: thesis: S₂[x,z]

now

per cases ( card ((the_Edges_of y') /\ (the_Edges_of G2)) > card ((the_Edges_of z') /\ (the_Edges_of G2)) or ( card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of z') /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y',ky] & S₁[z',kz] holds
ky >= kz ) ) ) by A30, A32, A33;

suppose card ((the_Edges_of y') /\ (the_Edges_of G2)) > card ((the_Edges_of z') /\ (the_Edges_of G2)) ; :: thesis: S₂[x,z]

hence S₂[x,z] by A31, A33, A34, XXREAL_0:2; :: thesis: verum

end;

suppose ( card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of z') /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y',ky] & S₁[z',kz] holds
ky >= kz ) ) ; :: thesis: S₂[x,z]

hence S₂[x,z] by A31, A33, A34; :: thesis: verum

end;

end;

end;

hence S₂[x,z] ; :: thesis: verum

end;

suppose A35: ( card ((the_Edges_of x') /\ (the_Edges_of G2)) = card ((the_Edges_of y') /\ (the_Edges_of G2)) & ( for kx, ky being Nat st S₁[x',kx] & S₁[y',ky] holds
kx >= ky ) ) ; :: thesis: S₂[x,z]

now

per cases ( card ((the_Edges_of y') /\ (the_Edges_of G2)) > card ((the_Edges_of z') /\ (the_Edges_of G2)) or ( card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of z') /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y',ky] & S₁[z',kz] holds
ky >= kz ) ) ) by A30, A32, A33;

suppose card ((the_Edges_of y') /\ (the_Edges_of G2)) > card ((the_Edges_of z') /\ (the_Edges_of G2)) ; :: thesis: S₂[x,z]

hence S₂[x,z] by A31, A33, A35; :: thesis: verum

end;

suppose A36: ( card ((the_Edges_of y') /\ (the_Edges_of G2)) = card ((the_Edges_of z') /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y',ky] & S₁[z',kz] holds
ky >= kz ) ) ; :: thesis: S₂[x,z]

consider zx being Nat;
consider zy being Nat such that
A37: S₁[y,zy] by A8;
consider zz being Nat;

now

let kx, kz be Nat; :: thesis: ( S₁[x',kx] & S₁[z',kz] implies kx >= kz )
assume ( S₁[x',kx] & S₁[z',kz] ) ; :: thesis: kx >= kz
then ( kx >= zy & zy >= kz ) by A32, A35, A36, A37;
hence kx >= kz by XXREAL_0:2; :: thesis: verum

end;

hence S₂[x,z] by A31, A33, A35, A36; :: thesis: verum

end;

end;

end;

hence S₂[x,z] ; :: thesis: verum

end;

end;

end;

hence S₂[x,z] ; :: thesis: verum

end;

then A38: for x, y, z being Element of X st S₂[x,y] & S₂[y,z] holds
S₂[x,z] ;
consider M being Element of X such that
A39: ( M in X & ( for y being Element of X st y in X holds
S₂[M,y] ) ) from CQC_SIM1:sch 4(A21, A29, A38);
consider x being Element of G1 .allWSubgraphs() such that
A40: ( M = x & x is minimumSpanningTree of G1 ) by A39;
reconsider M = M as minimumSpanningTree of G1 by A40;
A41: the_Vertices_of G2 = the_Vertices_of M by A4, GLIB_000:def 35;

A42: now

assume A43: the_Edges_of G2 = the_Edges_of M ; :: thesis: contradiction
the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10
.= the_Weight_of M by A43, GLIB_003:def 10 ;
hence contradiction by A6, A41, A43, Th36, GLIB_000:89; :: thesis: verum

end;

defpred S₃[ Nat] means not ((PRIM:CompSeq G1) . $1) `2 c= the_Edges_of M;

now

assume the_Edges_of G2 c= the_Edges_of M ; :: thesis: contradiction
then the_Edges_of G2 c< the_Edges_of M by A42, XBOOLE_0:def 8;
then (G2 .size() ) + 1 < (M .size() ) + 1 by CARD_2:67, XREAL_1:10;
then A44: G2 .order() < (M .size() ) + 1 by A5, GLIB_002:46;
G2 .order() = M .order() by A4, GLIB_000:def 35;
hence contradiction by A44, GLIB_002:46; :: thesis: verum

end;

then A45: ex k being Nat st S₃[k] by A4;
consider k being Nat such that
A46: ( S₃[k] & ( for n being Nat st S₃[n] holds
k <= n ) ) from NAT_1:sch 5(A45);

now

assume k = 0 ; :: thesis: contradiction
then A47: not (PRIM:Init G1) `2 c= the_Edges_of M by A46, Def15;
(PRIM:Init G1) `2 = {} by MCART_1:7;
hence contradiction by A47, XBOOLE_1:2; :: thesis: verum

end;

then consider k1o being Nat such that
A48: k = k1o + 1 by NAT_1:6;
set Gk1b = (PRIM:CompSeq G1) . k1o;
set Gk = (PRIM:CompSeq G1) . k;
A49: (PRIM:CompSeq G1) . k = PRIM:Step ((PRIM:CompSeq G1) . k1o) by A48, Def15;
(k1o + 1) - 1 < k - 0 by A48, XREAL_1:17;
then A50: ((PRIM:CompSeq G1) . k1o) `2 c= the_Edges_of M by A46;
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o);
set ep = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o));
A51: PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o) <> {} by A46, A49, A50, Def14;
then A52: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o) ;
consider v being Vertex of G1 such that
A53: ( not v in ((PRIM:CompSeq G1) . k1o) `1 & (PRIM:CompSeq G1) . k = [((((PRIM:CompSeq G1) . k1o) `1 ) \/ {v}),((((PRIM:CompSeq G1) . k1o) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})] ) by A49, A51, Lm6;
A54: ((PRIM:CompSeq G1) . k) `2 = (((PRIM:CompSeq G1) . k1o) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A53, MCART_1:7;
then A55: not {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} c= the_Edges_of M by A46, A50, XBOOLE_1:8;
then A56: not choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in the_Edges_of M by ZFMISC_1:37;
set V = ((PRIM:CompSeq G1) . k1o) `1 ;
A58: the_Vertices_of G1 = the_Vertices_of M by GLIB_000:def 35;
then reconsider V = ((PRIM:CompSeq G1) . k1o) `1 as non empty Subset of (the_Vertices_of M) by Lm9;
consider Mep being inducedWSubgraph of G1, the_Vertices_of G1,(the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))};
set v1 = (the_Source_of Mep) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)));
set v2 = (the_Target_of Mep) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)));
( {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} c= the_Edges_of G1 & the_Edges_of M c= the_Edges_of G1 ) by A52, ZFMISC_1:37;
then (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} c= the_Edges_of G1 by XBOOLE_1:8;
then ( the_Vertices_of G1 c= the_Vertices_of G1 & (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} c= G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:37;
then A59: ( the_Vertices_of Mep = the_Vertices_of G1 & the_Edges_of Mep = (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ) by GLIB_000:def 39;
then ( the_Vertices_of M c= the_Vertices_of Mep & the_Edges_of M c= the_Edges_of Mep ) by XBOOLE_1:7;
then reconsider M' = M as connected Subgraph of Mep by GLIB_000:47;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by TARSKI:def 1;
then A60: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in the_Edges_of Mep by A59, XBOOLE_0:def 3;
the_Vertices_of Mep = the_Vertices_of M by A59, GLIB_000:def 35;
then reconsider v1 = (the_Source_of Mep) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))), v2 = (the_Target_of Mep) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) as Vertex of M by A60, FUNCT_2:7;
consider W being Walk of M' such that
A61: W is_Walk_from v2,v1 by GLIB_002:def 1;
consider PW being Path of W;
A62: PW is_Walk_from v2,v1 by A61, GLIB_001:161;
A63: PW .edges() c= the_Edges_of M ;
reconsider P = PW as Path of Mep by GLIB_001:176;
A64: P .edges() c= the_Edges_of M by A63, GLIB_001:111;
A65: P is_Walk_from v2,v1 by A62, GLIB_001:20;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by TARSKI:def 1;
then A66: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in ((PRIM:CompSeq G1) . k) `2 by A54, XBOOLE_0:def 3;
A67: ((PRIM:CompSeq G1) . k) `2 c= (PRIM:MST G1) `2 by Th52;
then A68: {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} /\ (the_Edges_of G2) = {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A4, A66, ZFMISC_1:52;
A69: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) Joins v1,v2,Mep by A60, GLIB_000:def 15;
then choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) Joins v1,v2,G1 by GLIB_000:75;
then A70: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) Joins v1,v2,G2' by A4, A66, A67, GLIB_000:76;
then ( ( (the_Source_of G2) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v1 & (the_Target_of G2) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v2 ) or ( (the_Target_of G2) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v1 & (the_Source_of G2) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v2 ) ) by GLIB_000:def 15;
then v1 <> v2 by A4, A66, A67, A70, GLIB_000:def 20;
then v1 <> P .first() by A65, GLIB_001:def 23;
then P .last() <> P .first() by A65, GLIB_001:def 23;
then A71: not P is closed by GLIB_001:def 24;
A72: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) Joins P .last() ,v2,Mep by A65, A69, GLIB_001:def 23;
A73: not choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) in P .edges() by A55, A64, ZFMISC_1:37;

now

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len P implies not P . n = v2 )
assume A74: ( 1 < n & n <= len P & P . n = v2 ) ; :: thesis: contradiction
v2 = P .first() by A65, GLIB_001:def 23
.= P . ((2 * 0 ) + 1) by GLIB_001:def 6 ;
then n = len P by A74, GLIB_001:def 28;
then P .last() = v2 by A74, GLIB_001:def 7
.= P .first() by A65, GLIB_001:def 23 ;
then A75: P is closed by GLIB_001:def 24;
reconsider PM = P as Walk of M ;
( PM is Path-like & PM is closed & not PM is trivial ) by A74, A75, GLIB_001:127, GLIB_001:177;
then PM is Cycle-like by GLIB_001:def 31;
hence contradiction by GLIB_002:def 2; :: thesis: verum

end;

then A76: P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) is Path-like by A71, A72, A73, GLIB_001:151;
set C = P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)));
A77: not P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) is trivial by A72, GLIB_001:133;
P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) is_Walk_from v2,v2 by A65, A69, GLIB_001:67;
then P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) is closed by GLIB_001:120;
then A78: P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) is Cycle-like by A76, A77, GLIB_001:def 31;
A79: choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) SJoins ((PRIM:CompSeq G1) . k1o) `1 ,(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ),G1 by A51, Def12;
A80: ( (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v1 & (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) = v2 ) by A60, GLIB_000:def 34;
A81: ( v1 = P . (len P) & v2 = P . 1 ) by A62, GLIB_001:18;

now

per cases ( ( v1 in ((PRIM:CompSeq G1) . k1o) `1 & v2 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) ) or ( v2 in ((PRIM:CompSeq G1) . k1o) `1 & v1 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) ) ) by A79, A80, GLIB_000:def 17;

suppose A82: ( v1 in ((PRIM:CompSeq G1) . k1o) `1 & v2 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) ) ; :: thesis: ex em being set st
( em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() & em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )

defpred S₄[ Nat] means ( not $1 is even & $1 <= len P & P . $1 in ((PRIM:CompSeq G1) . k1o) `1 );
A83: ex n being Nat st S<sub>4</sub>[n] by A81, A82;
consider m being Nat such that
A84: ( S<sub>4</sub>[m] & ( for n being Nat st S<sub>4</sub>[n] holds
m <= n ) ) from NAT_1:sch 5(A83);
reconsider m = m as odd Element of NAT by A84, ORDINAL1:def 13;
A85: ( 1 <= m & m <= len P ) by A84, HEYTING3:1;
m <> 1 by A81, A82, A84, XBOOLE_0:def 5;
then 1 < m by A85, XXREAL_0:1;
then 1 + 1 <= m by NAT_1:13;
then reconsider m2k = m - (2 * 1) as odd Element of NAT by INT_1:18;
A86: m2k < m - 0 by XREAL_1:17;
then A87: m2k < len P by A84, XXREAL_0:2;
then A88: not P . m2k in ((PRIM:CompSeq G1) . k1o) `1 by A84, A86;
A89: m2k + 2 = m ;
set em = P . (m2k + 1);
take em = P . (m2k + 1); :: thesis: ( em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() & em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )
A90: em in P .edges() by A87, GLIB_001:101;
(P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() = (P .edges() ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A72, GLIB_001:112;
hence em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() by A90, XBOOLE_0:def 3; :: thesis: ( em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )
consider i being even Element of NAT such that
A91: ( 1 <= i & i <= len P & P . i = em ) by A90, GLIB_001:100;
i in dom P by A91, FINSEQ_3:27;
then A92: (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . i = em by A72, A91, GLIB_001:66;
A93: len (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) = (len P) + 2 by A72, GLIB_001:65;
A94: (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . ((len P) + 1) = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A72, GLIB_001:66;
(len P) + 0 < (len P) + 1 by XREAL_1:10;
then A95: i < (len P) + 1 by A91, XXREAL_0:2;
(len P) + 1 <= (len P) + 2 by XREAL_1:9;
hence em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A76, A91, A92, A93, A94, A95, GLIB_001:139; :: thesis: em SJoins V,(the_Vertices_of M) \ V,M
A97: em Joins PW . m2k,PW . m,M by A87, A89, GLIB_001:def 3;
then PW . m2k in the_Vertices_of M by GLIB_000:16;
then PW . m2k in (the_Vertices_of M) \ (((PRIM:CompSeq G1) . k1o) `1 ) by A88, XBOOLE_0:def 5;
hence em SJoins V,(the_Vertices_of M) \ V,M by A84, A97, GLIB_000:20; :: thesis: verum

end;

suppose A98: ( v2 in ((PRIM:CompSeq G1) . k1o) `1 & v1 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) ) ; :: thesis: ex em being set st
( em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() & em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )

defpred S₄[ Nat] means ( not $1 is even & $1 <= len P & P . $1 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) );
A99: ex n being Nat st S₄[n] by A81, A98;
consider m being Nat such that
A100: ( S₄[m] & ( for n being Nat st S₄[n] holds
m <= n ) ) from NAT_1:sch 5(A99);
reconsider m = m as odd Element of NAT by A100, ORDINAL1:def 13;
A101: ( 1 <= m & m <= len P ) by A100, HEYTING3:1;
m <> 1 by A81, A98, A100, XBOOLE_0:def 5;
then 1 < m by A101, XXREAL_0:1;
then 1 + 1 <= m by NAT_1:13;
then reconsider m2k = m - (2 * 1) as odd Element of NAT by INT_1:18;
A102: m2k < m - 0 by XREAL_1:17;
then A103: m2k < len P by A100, XXREAL_0:2;

A104: now

assume A105: not P . m2k in ((PRIM:CompSeq G1) . k1o) `1 ; :: thesis: contradiction
P . m2k in the_Vertices_of G1 by A58, A103, GLIB_001:8;
then P . m2k in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1 ) by A105, XBOOLE_0:def 5;
hence contradiction by A100, A102, A103; :: thesis: verum

end;

A106: m2k + 2 = m ;
set em = P . (m2k + 1);
take em = P . (m2k + 1); :: thesis: ( em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() & em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )
A107: em in P .edges() by A103, GLIB_001:101;
(P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() = (P .edges() ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A72, GLIB_001:112;
hence em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() by A107, XBOOLE_0:def 3; :: thesis: ( em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M )
consider i being even Element of NAT such that
A108: ( 1 <= i & i <= len P & P . i = em ) by A107, GLIB_001:100;
i in dom P by A108, FINSEQ_3:27;
then A109: (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . i = em by A72, A108, GLIB_001:66;
A110: len (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) = (len P) + 2 by A72, GLIB_001:65;
A111: (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . ((len P) + 1) = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A72, GLIB_001:66;
(len P) + 0 < (len P) + 1 by XREAL_1:10;
then A112: i < (len P) + 1 by A108, XXREAL_0:2;
(len P) + 1 <= (len P) + 2 by XREAL_1:9;
hence em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A76, A108, A109, A110, A111, A112, GLIB_001:139; :: thesis: em SJoins V,(the_Vertices_of M) \ V,M
em Joins PW . m2k,PW . m,M by A103, A106, GLIB_001:def 3;
hence em SJoins V,(the_Vertices_of M) \ V,M by A58, A100, A104, GLIB_000:20; :: thesis: verum

end;

end;

end;

then consider em being set such that
A114: ( em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() & em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) & em SJoins V,(the_Vertices_of M) \ V,M ) ;
A115: em SJoins V,(the_Vertices_of G1) \ V,G1 by A58, A114, GLIB_000:75;
then A116: (the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))) <= (the_Weight_of G1) . em by A51, Def12;
consider M2 being [Weighted] weight-inheriting removeEdge of Mep,em;
reconsider M2 = M2 as WSubgraph of G1 by GLIB_003:16;
( the_Vertices_of M c= the_Vertices_of Mep & the_Edges_of M c= the_Edges_of Mep ) by A59, XBOOLE_1:7;
then reconsider M' = M as connected Subgraph of Mep by GLIB_000:47;
the_Vertices_of M' = the_Vertices_of Mep by A59, GLIB_000:def 35;
then M' is spanning by GLIB_000:def 35;
then Mep is connected by GLIB_002:23;
then A117: M2 is connected by A78, A114, GLIB_002:5;
A118: the_Edges_of M2 = ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) \ {em} by A59, GLIB_000:54;

now

{em} c= (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A59, A114, ZFMISC_1:37;
then A119: M2 .size() = (card ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - (card {em}) by A118, CARD_2:63
.= (card ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - 1 by CARD_1:50
.= ((card (the_Edges_of M)) + 1) - 1 by A56, CARD_2:54
.= M .size() ;
M2 .order() = card (the_Vertices_of G1) by A59, GLIB_000:56
.= M .order() by GLIB_000:def 35 ;
hence M2 .order() = (M2 .size() ) + 1 by A119, GLIB_002:46; :: thesis: verum

end;

then A120: M2 is Tree-like by A117, GLIB_002:47;
set M2' = M2 .strict WGraphSelectors ;
A121: ( M2 .strict WGraphSelectors == M2 & the_Weight_of (M2 .strict WGraphSelectors ) = the_Weight_of M2 ) by Lm2;
then A122: the_Edges_of (M2 .strict WGraphSelectors ) = ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) \ {em} by A118, GLIB_000:def 36;
reconsider M2' = M2 .strict WGraphSelectors as WSubgraph of G1 by A121, GLIB_003:15;

now

thus M2' is Tree-like by A120, Lm2, GLIB_002:48; :: thesis: M2' is spanning
the_Vertices_of M2' = the_Vertices_of M2 by A121, GLIB_000:def 36
.= the_Vertices_of G1 by A59, GLIB_000:56 ;
hence M2' is spanning by GLIB_000:def 35; :: thesis: verum

end;

then reconsider M2' = M2' as spanning Tree-like WSubgraph of G1 ;

now

A123: G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 by GLIB_000:37;
then A124: ( the_Edges_of M c= G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 ) ;
the_Vertices_of G1 = the_Vertices_of M by GLIB_000:def 35;
then M is inducedWSubgraph of G1, the_Vertices_of G1, the_Edges_of M by A123, GLIB_000:def 39;
then A126: Mep .cost() = (M .cost() ) + ((the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) by A52, A56, A123, A124, Th34;
(M2 .cost() ) + ((the_Weight_of Mep) . em) = Mep .cost() by A114, Th33;
then A127: M2 .cost() = (Mep .cost() ) - ((the_Weight_of Mep) . em) ;
the_Weight_of Mep = (the_Weight_of G1) | (the_Edges_of Mep) by GLIB_003:def 10;
then M2 .cost() = ((M .cost() ) + ((the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))))) - ((the_Weight_of G1) . em) by A114, A126, A127, FUNCT_1:72;
hence M2' .cost() = ((M .cost() ) + ((the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))))) - ((the_Weight_of G1) . em) by A121, GLIB_000:def 36; :: thesis: verum

end;

then A128: ((M2' .cost() ) + ((the_Weight_of G1) . em)) - ((the_Weight_of G1) . em) <= ((M .cost() ) + ((the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o))))) - ((the_Weight_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) by A116, XREAL_1:15;

now

let G3 be spanning Tree-like WSubgraph of G1; :: thesis: M2' .cost() <= G3 .cost()
M .cost() <= G3 .cost() by Def17;
hence M2' .cost() <= G3 .cost() by A128, XXREAL_0:2; :: thesis: verum

end;

then reconsider M2' = M2' as minimumSpanningTree of G1 by Def17;
set MG2' = (the_Edges_of M2') /\ (the_Edges_of G2);
set MG2 = (the_Edges_of M) /\ (the_Edges_of G2);
A129: (the_Edges_of M2') /\ (the_Edges_of G2) = (((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2)) \ ({em} /\ (the_Edges_of G2)) by A122, XBOOLE_1:50;

now

assume ((the_Edges_of M) /\ (the_Edges_of G2)) /\ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} <> {} ; :: thesis: contradiction
then consider x being set such that
A130: x in ((the_Edges_of M) /\ (the_Edges_of G2)) /\ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by XBOOLE_0:def 1;
( x in (the_Edges_of M) /\ (the_Edges_of G2) & x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ) by A130, XBOOLE_0:def 4;
then ( x in the_Edges_of M & x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) ) by TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by A55, ZFMISC_1:37; :: thesis: verum

end;

then A131: (the_Edges_of M) /\ (the_Edges_of G2) misses {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by XBOOLE_0:def 7;
dom M2' = WGraphSelectors by Lm3;
then M2' in G1 .allWSubgraphs() by Def10;
then A132: M2' in X ;

A133: now

thus not ((PRIM:CompSeq G1) . (k1o + 1)) `2 c= the_Edges_of M by A46, A48; :: thesis: for n being Nat st n <= k1o holds
((PRIM:CompSeq G1) . n) `2 c= the_Edges_of M
let n be Nat; :: thesis: ( n <= k1o implies ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of M )
assume n <= k1o ; :: thesis: ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of M
then ((PRIM:CompSeq G1) . n) `2 c= ((PRIM:CompSeq G1) . k1o) `2 by Lm13;
hence ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of M by A50, XBOOLE_1:1; :: thesis: verum

end;

A134: now

assume A135: em in the_Edges_of G2 ; :: thesis: contradiction
then A136: (the_Edges_of M2') /\ (the_Edges_of G2) = (((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2)) \ {em} by A129, ZFMISC_1:52;

now

let x be set ; :: thesis: ( x in {em} implies x in ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2) )
assume x in {em} ; :: thesis: x in ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2)
then x = em by TARSKI:def 1;
hence x in ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2) by A59, A114, A135, XBOOLE_0:def 4; :: thesis: verum

end;

then {em} c= ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2) by TARSKI:def 3;
then A137: card ((the_Edges_of M2') /\ (the_Edges_of G2)) = (card ((the_Edges_of Mep) /\ (the_Edges_of G2))) - (card {em}) by A59, A136, CARD_2:63
.= (card ((the_Edges_of Mep) /\ (the_Edges_of G2))) - 1 by CARD_1:50
.= (card (((the_Edges_of M) /\ (the_Edges_of G2)) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - 1 by A59, A68, XBOOLE_1:23
.= ((card ((the_Edges_of M) /\ (the_Edges_of G2))) + (card {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - 1 by A131, CARD_2:53
.= ((card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1) - 1 by CARD_1:50
.= card ((the_Edges_of M) /\ (the_Edges_of G2)) ;
consider k2 being Nat such that
A138: S₁[M2',k2] by A8, A132;

A139: now

set Vr = (the_Vertices_of G1) \ V;
assume A140: em in ((PRIM:CompSeq G1) . k1o) `2 ; :: thesis: contradiction
((PRIM:CompSeq G1) . k1o) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . k1o) `1 ) by Lm9;
then ( (the_Source_of G1) . em in ((PRIM:CompSeq G1) . k1o) `1 & (the_Target_of G1) . em in ((PRIM:CompSeq G1) . k1o) `1 ) by A140, GLIB_000:34;
then ( not (the_Source_of G1) . em in (the_Vertices_of G1) \ V & not (the_Target_of G1) . em in (the_Vertices_of G1) \ V ) by XBOOLE_0:def 5;
hence contradiction by A115, GLIB_000:def 17; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G1) . k) `2 implies x in the_Edges_of M2' )
assume A141: x in ((PRIM:CompSeq G1) . k) `2 ; :: thesis: x in the_Edges_of M2'

now

per cases ( x in ((PRIM:CompSeq G1) . k1o) `2 or x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ) by A54, A141, XBOOLE_0:def 3;

suppose A142: x in ((PRIM:CompSeq G1) . k1o) `2 ; :: thesis: x in the_Edges_of M2'

then A143: x in (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A50, XBOOLE_0:def 3;
not x in {em} by A139, A142, TARSKI:def 1;
hence x in the_Edges_of M2' by A122, A143, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A144: x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ; :: thesis: x in the_Edges_of M2'

then A145: x in (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by XBOOLE_0:def 3;
x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A144, TARSKI:def 1;
then not x in {em} by A114, TARSKI:def 1;
hence x in the_Edges_of M2' by A122, A145, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence x in the_Edges_of M2' ; :: thesis: verum

end;

then A146: ((PRIM:CompSeq G1) . k) `2 c= the_Edges_of M2' by TARSKI:def 3;

A147: now

assume k2 < k ; :: thesis: contradiction
then k2 + 1 <= k by NAT_1:13;
then ((PRIM:CompSeq G1) . (k2 + 1)) `2 c= ((PRIM:CompSeq G1) . k) `2 by Lm13;
hence contradiction by A138, A146, XBOOLE_1:1; :: thesis: verum

end;

A148: k1o >= k2 by A39, A132, A133, A137, A138;
(k1o + 1) - 1 < k - 0 by A48, XREAL_1:17;
hence contradiction by A147, A148, XXREAL_0:2; :: thesis: verum

end;

now

assume {em} /\ (the_Edges_of G2) <> {} ; :: thesis: contradiction
then consider x being set such that
A149: x in {em} /\ (the_Edges_of G2) by XBOOLE_0:def 1;
( x in {em} & x in the_Edges_of G2 ) by A149, XBOOLE_0:def 4;
hence contradiction by A134, TARSKI:def 1; :: thesis: verum

end;

then A150: (the_Edges_of M2') /\ (the_Edges_of G2) = ((the_Edges_of M) /\ (the_Edges_of G2)) \/ ({(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} /\ (the_Edges_of G2)) by A129, XBOOLE_1:23;

now

assume ((the_Edges_of M) /\ (the_Edges_of G2)) /\ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} <> {} ; :: thesis: contradiction
then consider x being set such that
A151: x in ((the_Edges_of M) /\ (the_Edges_of G2)) /\ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by XBOOLE_0:def 1;
( x in (the_Edges_of M) /\ (the_Edges_of G2) & x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ) by A151, XBOOLE_0:def 4;
then ( x in the_Edges_of M & x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) ) by TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by A55, ZFMISC_1:37; :: thesis: verum

end;

then (the_Edges_of M) /\ (the_Edges_of G2) misses {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by XBOOLE_0:def 7;
then card ((the_Edges_of M2') /\ (the_Edges_of G2)) = (card ((the_Edges_of M) /\ (the_Edges_of G2))) + (card {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) by A68, A150, CARD_2:53
.= (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1 by CARD_1:50 ;
then (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 0 >= (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1 by A39, A132;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

hence G2 is minimumSpanningTree of G1 ; :: thesis: verum