let G1 be finite connected real-weighted WGraph; :: thesis:
set PMST = PRIM:MST G1;
let G2 be inducedWSubgraph of G1,(PRIM:MST G1) `1 ,(PRIM:MST G1) `2 ; :: thesis:
reconsider G29 = G2 as Tree-like _Graph by Th38;
set VG1 = the_Vertices_of G1;
set EG1 = the_Edges_of G1;
set WG1 = the_Weight_of G1;
set PCS = PRIM:CompSeq G1;
A1: (PRIM:MST G1) `1 = the_Vertices_of G1 by Th39;
(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 A2: (PRIM:MST G1) `2 c= G1 .edgesBetween ((PRIM:MST G1) `1) by A1, GLIB_000:34;
A3: (PRIM:MST G1) `1 c= the_Vertices_of G1 by Th39;
then A4: the_Vertices_of G2 = the_Vertices_of G1 by A1, A2, GLIB_000:def 37;
A5: the_Edges_of G2 = (PRIM:MST G1) `2 by A1, A2, A3, GLIB_000:def 37;
A6: G2 is Tree-like by Th38;

now

set X = { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } ;

now

let x be set ; :: thesis:
assume x in { x where x is Element of G1 .allWSubgraphs() : x is minimumSpanningTree of G1 } ; :: thesis:
then ex G2 being Element of G1 .allWSubgraphs() st
( x = G2 & G2 is minimumSpanningTree of G1 ) ;
hence x in G1 .allWSubgraphs() ; :: thesis:

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;
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 ) ) );
A7: G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 by GLIB_000:34;

now

set M = the minimumSpanningTree of G1;
set M9 = the minimumSpanningTree of G1 | WGraphSelectors;
( the minimumSpanningTree of G1 | WGraphSelectors == the minimumSpanningTree of G1 & the_Weight_of ( the minimumSpanningTree of G1 | WGraphSelectors) = the_Weight_of the minimumSpanningTree of G1 ) by Lm4;
then reconsider M9 = the minimumSpanningTree of G1 | WGraphSelectors as minimumSpanningTree of G1 by Th41;
dom M9 = WGraphSelectors by Lm5;
then M9 in G1 .allWSubgraphs() by Def5;
then M9 in X ;
hence X <> {} ; :: thesis:

end;

then reconsider X = X as non empty finite Subset of (G1 .allWSubgraphs()) ;
assume A8: G2 is not minimumSpanningTree of G1 ; :: thesis:

A9: now

let G be Element of X; :: thesis:
G in X ;
then ex G9 being Element of G1 .allWSubgraphs() st
( G = G9 & G9 is minimumSpanningTree of G1 ) ;
then reconsider G9 = G as minimumSpanningTree of G1 ;
defpred S₃[ Nat] means not ((PRIM:CompSeq G1) . $1) `2 c= the_Edges_of G9;
A10: the_Vertices_of G2 = the_Vertices_of G9 by A4, GLIB_000:def 33;

A11: now

assume A12: the_Edges_of G2 = the_Edges_of G9 ; :: thesis:
the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10
.= the_Weight_of G9 by A12, GLIB_003:def 10 ;
hence contradiction by A8, A10, A12, Th41, GLIB_000:86; :: thesis:

end;

now

assume the_Edges_of G2 c= the_Edges_of G9 ; :: thesis:
then the_Edges_of G2 c< the_Edges_of G9 by A11, XBOOLE_0:def 8;
then (G2 .size()) + 1 < (G9 .size()) + 1 by CARD_2:48, XREAL_1:8;
then A13: G2 .order() < (G9 .size()) + 1 by A6, GLIB_002:46;
G2 .order() = G9 .order() by A4, GLIB_000:def 33;
hence contradiction by A13, GLIB_002:46; :: thesis:

end;

then A14: ex n being Nat st S₃[n] by A5;
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:
then A16: not (PRIM:Init G1) `2 c= the_Edges_of G9 by A15, Def17;
(PRIM:Init G1) `2 = {} by MCART_1:7;
hence contradiction by A16, XBOOLE_1:2; :: thesis:

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:15;
then A18: ((PRIM:CompSeq G1) . k2) `2 c= the_Edges_of G9 by A15;

now

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

end;

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

end;

now

let x, y, z be Element of X; :: thesis:
assume that
A19: S₂[x,y] and
A20: S₂[y,z] ; :: thesis:
y in X ;
then consider y9 being WSubgraph of G1 such that
A21: y9 = y and
dom y9 = WGraphSelectors by Def5;
set CY = card ((the_Edges_of y9) /\ (the_Edges_of G2));
x in X ;
then consider x9 being WSubgraph of G1 such that
A22: x9 = x and
dom x9 = WGraphSelectors by Def5;
z in X ;
then consider z9 being WSubgraph of G1 such that
A23: z9 = z and
dom z9 = WGraphSelectors by Def5;
set CZ = card ((the_Edges_of z9) /\ (the_Edges_of G2));
set CX = card ((the_Edges_of x9) /\ (the_Edges_of G2));

now

per cases by A19, A22, A21;

suppose A24: card ((the_Edges_of x9) /\ (the_Edges_of G2)) > card ((the_Edges_of y9) /\ (the_Edges_of G2)) ; :: thesis:

now

per cases by A20, A21, A23;

suppose card ((the_Edges_of y9) /\ (the_Edges_of G2)) > card ((the_Edges_of z9) /\ (the_Edges_of G2)) ; :: thesis:

hence S₂[x,z] by A22, A23, A24, XXREAL_0:2; :: thesis:

end;

suppose ( card ((the_Edges_of y9) /\ (the_Edges_of G2)) = card ((the_Edges_of z9) /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y9,ky] & S₁[z9,kz] holds
ky >= kz ) ) ; :: thesis:

hence S₂[x,z] by A22, A23, A24; :: thesis:

end;

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

end;

suppose A25: ( card ((the_Edges_of x9) /\ (the_Edges_of G2)) = card ((the_Edges_of y9) /\ (the_Edges_of G2)) & ( for kx, ky being Nat st S₁[x9,kx] & S₁[y9,ky] holds
kx >= ky ) ) ; :: thesis:

now

per cases by A20, A21, A23;

suppose card ((the_Edges_of y9) /\ (the_Edges_of G2)) > card ((the_Edges_of z9) /\ (the_Edges_of G2)) ; :: thesis:

hence S₂[x,z] by A22, A23, A25; :: thesis:

end;

suppose A26: ( card ((the_Edges_of y9) /\ (the_Edges_of G2)) = card ((the_Edges_of z9) /\ (the_Edges_of G2)) & ( for ky, kz being Nat st S₁[y9,ky] & S₁[z9,kz] holds
ky >= kz ) ) ; :: thesis:

consider zy being Nat such that
A27: S₁[y,zy] by A9;

now

let kx, kz be Nat; :: thesis:
assume ( S₁[x9,kx] & S₁[z9,kz] ) ; :: thesis:
then ( kx >= zy & zy >= kz ) by A21, A25, A26, A27;
hence kx >= kz by XXREAL_0:2; :: thesis:

end;

hence S₂[x,z] by A22, A23, A25, A26; :: thesis:

end;

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

end;

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

end;

then A28: for x, y, z being Element of X st S₂[x,y] & S₂[y,z] holds
S₂[x,z] ;

A29: now

let G be Element of X; :: thesis:
let k1, k2 be Nat; :: thesis:
assume A30: ( S₁[G,k1] & S₁[G,k2] ) ; :: thesis:
then k2 + 1 > k1 ;
then A31: k2 >= k1 by NAT_1:13;
k1 + 1 > k2 by A30;
then k1 >= k2 by NAT_1:13;
hence k1 = k2 by A31, XXREAL_0:1; :: thesis:

end;

now

let x, y be Element of X; :: thesis:
x in X ;
then consider x9 being WSubgraph of G1 such that
A32: x9 = x and
dom x9 = WGraphSelectors by Def5;
set CX = card ((the_Edges_of x9) /\ (the_Edges_of G2));
y in X ;
then consider y9 being WSubgraph of G1 such that
A33: y9 = y and
dom y9 = WGraphSelectors by Def5;
set CY = card ((the_Edges_of y9) /\ (the_Edges_of G2));

now

per cases by XXREAL_0:1;

suppose card ((the_Edges_of x9) /\ (the_Edges_of G2)) < card ((the_Edges_of y9) /\ (the_Edges_of G2)) ; :: thesis:

hence ( S₂[x,y] or S₂[y,x] ) by A32, A33; :: thesis:

end;

suppose A34: card ((the_Edges_of y9) /\ (the_Edges_of G2)) = card ((the_Edges_of x9) /\ (the_Edges_of G2)) ; :: thesis:

consider k1 being Nat such that
A35: S₁[x,k1] by A9;
consider k2 being Nat such that
A36: S₁[y,k2] by A9;

now

per cases ;

suppose A37: k1 >= k2 ; :: thesis:

now

let z1, z2 be Nat; :: thesis:
assume that
A38: S₁[x,z1] and
A39: S₁[y,z2] ; :: thesis:
z1 = k1 by A29, A35, A38;
hence z1 >= z2 by A29, A36, A37, A39; :: thesis:

end;

hence ( S₂[x,y] or S₂[y,x] ) by A32, A33, A34; :: thesis:

end;

suppose A40: k1 < k2 ; :: thesis:

now

let z1, z2 be Nat; :: thesis:
assume that
A41: S₁[x,z1] and
A42: S₁[y,z2] ; :: thesis:
z1 = k1 by A29, A35, A41;
hence z1 <= z2 by A29, A36, A40, A42; :: thesis:

end;

hence ( S₂[x,y] or S₂[y,x] ) by A32, A33, A34; :: thesis:

end;

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

end;

suppose card ((the_Edges_of x9) /\ (the_Edges_of G2)) > card ((the_Edges_of y9) /\ (the_Edges_of G2)) ; :: thesis:

hence ( S₂[x,y] or S₂[y,x] ) by A32, A33; :: thesis:

end;

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

end;

then A43: for x, y being Element of X holds
( S₂[x,y] or S₂[y,x] ) ;
A44: ( X is finite & X <> {} & X c= X ) ;
consider M being Element of X such that
A45: ( M in X & ( for y being Element of X st y in X holds
S₂[M,y] ) ) from CQC_SIM1:sch 4(A44, A43, A28);
ex x being Element of G1 .allWSubgraphs() st
( M = x & x is minimumSpanningTree of G1 ) by A45;
then reconsider M = M as minimumSpanningTree of G1 ;
defpred S₃[ Nat] means not ((PRIM:CompSeq G1) . $1) `2 c= the_Edges_of M;
A46: the_Vertices_of G2 = the_Vertices_of M by A4, GLIB_000:def 33;

A47: now

assume A48: the_Edges_of G2 = the_Edges_of M ; :: thesis:
the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10
.= the_Weight_of M by A48, GLIB_003:def 10 ;
hence contradiction by A8, A46, A48, Th41, GLIB_000:86; :: thesis:

end;

now

assume the_Edges_of G2 c= the_Edges_of M ; :: thesis:
then the_Edges_of G2 c< the_Edges_of M by A47, XBOOLE_0:def 8;
then (G2 .size()) + 1 < (M .size()) + 1 by CARD_2:48, XREAL_1:8;
then A49: G2 .order() < (M .size()) + 1 by A6, GLIB_002:46;
G2 .order() = M .order() by A4, GLIB_000:def 33;
hence contradiction by A49, GLIB_002:46; :: thesis:

end;

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

now

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

end;

now

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

end;

A78: now

reconsider PM = P as Walk of M ;
let n be odd Element of NAT ; :: thesis:
assume that
A79: ( 1 < n & n <= len P ) and
A80: P . n = v2 ; :: thesis:
v2 = P .first() by A77, GLIB_001:def 23
.= P . ((2 * 0) + 1) by GLIB_001:def 6 ;
then n = len P by A79, A80, GLIB_001:def 28;
then P .last() = v2 by A80, GLIB_001:def 7
.= P .first() by A77, GLIB_001:def 23 ;
then P is closed by GLIB_001:def 24;
then A81: PM is closed by GLIB_001:176;
not PM is trivial by A79, GLIB_001:126;
then PM is Cycle-like by A81, GLIB_001:def 31;
hence contradiction by GLIB_002:def 2; :: thesis:

end;

now

per cases by A57, A91, GLIB_000:def 15;

suppose A92: ( v1 in ((PRIM:CompSeq G1) . k1o) `1 & v2 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1) ) ; :: thesis:

end;

suppose A106: ( v2 in ((PRIM:CompSeq G1) . k1o) `1 & v1 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1) ) ; :: thesis:

A107: ( len (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) = (len P) + 2 & (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . ((len P) + 1) = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) ) by A83, GLIB_001:64, GLIB_001:65;
defpred S₄[ Nat] means ( not $1 is even & $1 <= len P & P . $1 in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1) );
A108: ex n being Nat st S₄[n] by A90, A106;
consider m being Nat such that
A109: ( S₄[m] & ( for n being Nat st S₄[n] holds
m <= n ) ) from NAT_1:sch 5(A108);
reconsider m = m as odd Element of NAT by A109, ORDINAL1:def 12;
( 1 <= m & m <> 1 ) by A89, A106, A109, ABIAN:12, XBOOLE_0:def 5;
then 1 < m by 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:5;
A110: m2k < m - 0 by XREAL_1:15;
then A111: m2k < len P by A109, XXREAL_0:2;

A112: now

assume A113: not P . m2k in ((PRIM:CompSeq G1) . k1o) `1 ; :: thesis:
P . m2k in the_Vertices_of G1 by A72, A111, GLIB_001:7;
then P . m2k in (the_Vertices_of G1) \ (((PRIM:CompSeq G1) . k1o) `1) by A113, XBOOLE_0:def 5;
hence contradiction by A109, A110, A111; :: thesis:

end;

set em = P . (m2k + 1);
A114: P . (m2k + 1) in P .edges() by A111, GLIB_001:100;
then consider i being even Element of NAT such that
A115: 1 <= i and
A116: i <= len P and
A117: P . i = P . (m2k + 1) by GLIB_001:99;
i in dom P by A115, A116, FINSEQ_3:25;
then A118: (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) . i = P . (m2k + 1) by A83, A117, GLIB_001:65;
take em = P . (m2k + 1); :: thesis:
(P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() = (P .edges()) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A83, GLIB_001:111;
hence em in (P .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))) .edges() by A114, XBOOLE_0:def 3; :: thesis:
A119: (len P) + 1 <= (len P) + 2 by XREAL_1:7;
(len P) + 0 < (len P) + 1 by XREAL_1:8;
then i < (len P) + 1 by A116, XXREAL_0:2;
hence em <> choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by A86, A115, A118, A107, A119, GLIB_001:138; :: thesis:
m2k + 2 = m ;
then em Joins the Path of W . m2k, the Path of W . m,M by A111, GLIB_001:def 3;
hence em SJoins V,(the_Vertices_of M) \ V,M by A72, A109, A112, GLIB_000:17; :: thesis:

end;

now

let G3 be spanning Tree-like WSubgraph of G1; :: thesis:
M .cost() <= G3 .cost() by Def19;
hence M29 .cost() <= G3 .cost() by A132, XXREAL_0:2; :: thesis:

end;

then reconsider M29 = M29 as minimumSpanningTree of G1 by Def19;
set MG29 = (the_Edges_of M29) /\ (the_Edges_of G2);
A133: (the_Edges_of M29) /\ (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 A128, XBOOLE_1:50;
dom M29 = WGraphSelectors by Lm5;
then M29 in G1 .allWSubgraphs() by Def5;
then A134: M29 in X ;

A135: now

thus not ((PRIM:CompSeq G1) . (k1o + 1)) `2 c= the_Edges_of M by A51, A53; :: thesis:
let n be Nat; :: thesis:
assume n <= k1o ; :: thesis:
then ((PRIM:CompSeq G1) . n) `2 c= ((PRIM:CompSeq G1) . k1o) `2 by Th34;
hence ((PRIM:CompSeq G1) . n) `2 c= the_Edges_of M by A54, XBOOLE_1:1; :: thesis:

end;

A136: now

consider k2 being Nat such that
A137: S₁[M29,k2] by A9, A134;

A138: now

set Vr = (the_Vertices_of G1) \ V;
assume A139: em in ((PRIM:CompSeq G1) . k1o) `2 ; :: thesis:
A140: ((PRIM:CompSeq G1) . k1o) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . k1o) `1) by Th30;
then (the_Target_of G1) . em in ((PRIM:CompSeq G1) . k1o) `1 by A139, GLIB_000:31;
then A141: not (the_Target_of G1) . em in (the_Vertices_of G1) \ V by XBOOLE_0:def 5;
(the_Source_of G1) . em in ((PRIM:CompSeq G1) . k1o) `1 by A139, A140, GLIB_000:31;
then not (the_Source_of G1) . em in (the_Vertices_of G1) \ V by XBOOLE_0:def 5;
hence contradiction by A124, A141, GLIB_000:def 15; :: thesis:

end;

now

let x be set ; :: thesis:
assume A142: x in ((PRIM:CompSeq G1) . k) `2 ; :: thesis:

now

per cases by A58, A142, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G1) . k1o) `2 ; :: thesis:

then ( x in (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} & not x in {em} ) by A54, A138, TARSKI:def 1, XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A128, XBOOLE_0:def 5; :: thesis:

end;

suppose A143: x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} ; :: thesis:

then x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) by TARSKI:def 1;
then A144: not x in {em} by A121, TARSKI:def 1;
x in (the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} by A143, XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A128, A144, XBOOLE_0:def 5; :: thesis:

end;

hence x in the_Edges_of M29 ; :: thesis:

end;

then A145: ((PRIM:CompSeq G1) . k) `2 c= the_Edges_of M29 by TARSKI:def 3;

A146: now

assume k2 < k ; :: thesis:
then k2 + 1 <= k by NAT_1:13;
then ((PRIM:CompSeq G1) . (k2 + 1)) `2 c= ((PRIM:CompSeq G1) . k) `2 by Th34;
hence contradiction by A137, A145, XBOOLE_1:1; :: thesis:

end;

assume A147: em in the_Edges_of G2 ; :: thesis:

now

let x be set ; :: thesis:
assume x in {em} ; :: thesis:
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 A73, A120, A147, XBOOLE_0:def 4; :: thesis:

end;

then A148: {em} c= ((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2) by TARSKI:def 3;
(the_Edges_of M29) /\ (the_Edges_of G2) = (((the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2)) \ {em} by A133, A147, ZFMISC_1:46;
then card ((the_Edges_of M29) /\ (the_Edges_of G2)) = (card ((the_Edges_of the inducedWSubgraph of G1, the_Vertices_of G1,(the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2))) - (card {em}) by A73, A148, CARD_2:44
.= (card ((the_Edges_of the inducedWSubgraph of G1, the_Vertices_of G1,(the_Edges_of M) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) /\ (the_Edges_of G2))) - 1 by CARD_1:30
.= (card (((the_Edges_of M) /\ (the_Edges_of G2)) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - 1 by A73, A67, XBOOLE_1:23
.= ((card ((the_Edges_of M) /\ (the_Edges_of G2))) + (card {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))})) - 1 by A70, CARD_2:40
.= ((card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1) - 1 by CARD_1:30
.= card ((the_Edges_of M) /\ (the_Edges_of G2)) ;
then A149: k1o >= k2 by A45, A134, A135, A137;
(k1o + 1) - 1 < k - 0 by A53, XREAL_1:15;
hence contradiction by A146, A149, XXREAL_0:2; :: thesis:

end;

now

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

end;

then A151: (the_Edges_of M29) /\ (the_Edges_of G2) = ((the_Edges_of M) /\ (the_Edges_of G2)) \/ ({(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))} /\ (the_Edges_of G2)) by A133, XBOOLE_1:23;

now

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

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 M29) /\ (the_Edges_of G2)) = (card ((the_Edges_of M) /\ (the_Edges_of G2))) + (card {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)))}) by A67, A151, CARD_2:40
.= (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1 by CARD_1:30 ;
then (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 0 >= (card ((the_Edges_of M) /\ (the_Edges_of G2))) + 1 by A45, A134;
hence contradiction by XREAL_1:6; :: thesis:

end;

hence G2 is minimumSpanningTree of G1 ; :: thesis: