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 c= the_Edges_of G1 ;
then A2: (PRIM:MST G1) `2 c= G1 .edgesBetween ((PRIM:MST G1) `1) by A1, GLIB_000:34;
A3: the_Vertices_of G2 = the_Vertices_of G1 by A1, A2, GLIB_000:def 37;
A4: the_Edges_of G2 = (PRIM:MST G1) `2 by A1, A2, GLIB_000:def 37;
A5: G2 is Tree-like by Th38;

now :: thesis:

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

now :: thesis:

let x be object ; :: 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 ) ) );
A6: G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 by GLIB_000:34;

now :: thesis:

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 A7: G2 is not minimumSpanningTree of G1 ; :: thesis:

A8: now :: thesis:

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;
A9: the_Vertices_of G2 = the_Vertices_of G9 by A3, GLIB_000:def 33;

A10: now :: thesis:

assume A11: 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 A11, GLIB_003:def 10 ;
hence contradiction by A7, A9, A11, Th41, GLIB_000:86; :: thesis:

end;

now :: thesis:

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

end;

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

now :: thesis:

assume k3 = 0 ; :: thesis:
then not (PRIM:Init G1) `2 c= the_Edges_of G9 by A14, Def17;
hence contradiction ; :: thesis:

end;

then consider k2 being Nat such that
A16: k2 + 1 = k3 by NAT_1:6;
(k2 + 1) - 1 < k3 - 0 by A16, XREAL_1:15;
then A17: ((PRIM:CompSeq G1) . k2) `2 c= the_Edges_of G9 by A14;

now :: thesis:

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 A17; :: thesis:

end;

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

end;

now :: thesis:

let x, y, z be Element of X; :: thesis:
assume that
A18: S₂[x,y] and
A19: S₂[y,z] ; :: thesis:
y in X ;
then consider y9 being WSubgraph of G1 such that
A20: 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
A21: x9 = x and
dom x9 = WGraphSelectors by Def5;
z in X ;
then consider z9 being WSubgraph of G1 such that
A22: 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 :: thesis:

per cases by A18, A21, A20;

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

now :: thesis:

per cases by A19, A20, A22;

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 A21, A22, A23, 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 A21, A22, A23; :: thesis:

end;

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

end;

suppose A24: ( 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 :: thesis:

per cases by A19, A20, A22;

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 A21, A22, A24; :: thesis:

end;

suppose A25: ( 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
A26: S₁[y,zy] by A8;

now :: thesis:

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

end;

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

end;

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

end;

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

end;

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

A28: now :: thesis:

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

end;

now :: thesis:

let x, y be Element of X; :: thesis:
x in X ;
then consider x9 being WSubgraph of G1 such that
A31: 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
A32: y9 = y and
dom y9 = WGraphSelectors by Def5;
set CY = card ((the_Edges_of y9) /\ (the_Edges_of G2));

now :: thesis:

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 A31, A32; :: thesis:

end;

suppose A33: 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
A34: S₁[x,k1] by A8;
consider k2 being Nat such that
A35: S₁[y,k2] by A8;

now :: thesis:

per cases ;

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

now :: thesis:

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

end;

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

end;

suppose A39: k1 < k2 ; :: thesis:

now :: thesis:

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

end;

hence ( S₂[x,y] or S₂[y,x] ) by A31, A32, A33; :: 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 A31, A32; :: thesis:

end;

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

end;

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

A46: now :: thesis:

assume A47: 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 A47, GLIB_003:def 10 ;
hence contradiction by A7, A45, A47, Th41, GLIB_000:86; :: thesis:

end;

now :: thesis:

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

end;

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

now :: thesis:

assume k = 0 ; :: thesis:
then not (PRIM:Init G1) `2 c= the_Edges_of M by A50, Def17;
hence contradiction ; :: thesis:

end;

now :: thesis:

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

end;

A77: now :: thesis:

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

end;

now :: thesis:

per cases by A56, A90;

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

end;

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

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

A111: now :: thesis:

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

end;

set em = P . (m2k + 1);
A113: P . (m2k + 1) in P .edges() by A110, GLIB_001:100;
then consider i being even Element of NAT such that
A114: 1 <= i and
A115: i <= len P and
A116: P . i = P . (m2k + 1) by GLIB_001:99;
i in dom P by A114, A115, FINSEQ_3:25;
then A117: (P .addEdge the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) . i = P . (m2k + 1) by A82, A116, GLIB_001:65;
take em = P . (m2k + 1); :: thesis:
(P .addEdge the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) .edges() = (P .edges()) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)} by A82, GLIB_001:111;
hence em in (P .addEdge the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)) .edges() by A113, XBOOLE_0:def 3; :: thesis:
A118: (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 A115, XXREAL_0:2;
hence em <> the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o) by A85, A114, A117, A106, A118, GLIB_001:138; :: thesis:
m2k + 2 = m ;
then em Joins the Path of W . m2k, the Path of W . m,M by A110, GLIB_001:def 3;
hence em SJoins V,(the_Vertices_of M) \ V,M by A71, A108, A111; :: thesis:

end;

now :: thesis:

let G3 be spanning Tree-like WSubgraph of G1; :: thesis:
M .cost() <= G3 .cost() by Def19;
hence M29 .cost() <= G3 .cost() by A131, 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);
A132: (the_Edges_of M29) /\ (the_Edges_of G2) = (((the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2)) \ ({em} /\ (the_Edges_of G2)) by A127, XBOOLE_1:50;
dom M29 = WGraphSelectors by Lm5;
then M29 in G1 .allWSubgraphs() by Def5;
then A133: M29 in X ;

A134: now :: thesis:

thus not ((PRIM:CompSeq G1) . (k1o + 1)) `2 c= the_Edges_of M by A50, A52; :: 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 A53; :: thesis:

end;

A135: now :: thesis:

consider k2 being Nat such that
A136: S₁[M29,k2] by A8, A133;

A137: now :: thesis:

set Vr = (the_Vertices_of G1) \ V;
assume A138: em in ((PRIM:CompSeq G1) . k1o) `2 ; :: thesis:
A139: ((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 A138, GLIB_000:31;
then A140: 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 A138, A139, GLIB_000:31;
then not (the_Source_of G1) . em in (the_Vertices_of G1) \ V by XBOOLE_0:def 5;
hence contradiction by A123, A140; :: thesis:

end;

now :: thesis:

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

now :: thesis:

per cases by A57, A141, XBOOLE_0:def 3;

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

then ( x in (the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)} & not x in {em} ) by A53, A137, TARSKI:def 1, XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A127, XBOOLE_0:def 5; :: thesis:

end;

suppose A142: x in { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)} ; :: thesis:

then x = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o) by TARSKI:def 1;
then A143: not x in {em} by A120, TARSKI:def 1;
x in (the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)} by A142, XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A127, A143, XBOOLE_0:def 5; :: thesis:

end;

hence x in the_Edges_of M29 ; :: thesis:

end;

then A144: ((PRIM:CompSeq G1) . k) `2 c= the_Edges_of M29 ;

A145: now :: thesis:

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 A136, A144, XBOOLE_1:1; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in {em} ; :: thesis:
then x = em by TARSKI:def 1;
hence x in ((the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2) by A72, A119, A146, XBOOLE_0:def 4; :: thesis:

end;

then A147: {em} c= ((the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2) ;
(the_Edges_of M29) /\ (the_Edges_of G2) = (((the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2)) \ {em} by A132, A146, 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) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2))) - (card {em}) by A72, A147, CARD_2:44
.= (card ((the_Edges_of the inducedWSubgraph of G1, the_Vertices_of G1,(the_Edges_of M) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) /\ (the_Edges_of G2))) - 1 by CARD_1:30
.= (card (((the_Edges_of M) /\ (the_Edges_of G2)) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)})) - 1 by A72, A66, XBOOLE_1:23
.= ((card ((the_Edges_of M) /\ (the_Edges_of G2))) + (card { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)})) - 1 by A69, 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 A148: k1o >= k2 by A44, A133, A134, A136;
(k1o + 1) - 1 < k - 0 by A52, XREAL_1:15;
hence contradiction by A145, A148, XXREAL_0:2; :: thesis:

end;

now :: thesis:

assume {em} /\ (the_Edges_of G2) <> {} ; :: thesis:
then consider x being object 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 A135, TARSKI:def 1; :: thesis:

end;

then A150: (the_Edges_of M29) /\ (the_Edges_of G2) = ((the_Edges_of M) /\ (the_Edges_of G2)) \/ ({ the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)} /\ (the_Edges_of G2)) by A132, XBOOLE_1:23;

now :: thesis:

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

end;

then (the_Edges_of M) /\ (the_Edges_of G2) misses { the Element of 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 { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G1) . k1o)}) by A66, A150, 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 A44, A133;
hence contradiction by XREAL_1:6; :: thesis:

end;

hence G2 is minimumSpanningTree of G1 ; :: thesis: