let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds
( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )
let n be Nat; :: thesis: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )
set src = the Element of the_Vertices_of G;
set PCS = PRIM:CompSeq G;
set RFS = G .reachableFrom the Element of the_Vertices_of G;
set Gn = (PRIM:CompSeq G) . n;
set EG = the_Edges_of G;
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set GnV = ((PRIM:CompSeq G) . n) `1 ;
set GnVg = (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);

hereby :: thesis: ( ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G implies PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} )

assume A1: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G

now :: thesis: not ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the Element of the_Vertices_of G

defpred S₁[ set ] means $1 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G;
assume A2: ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the Element of the_Vertices_of G ; :: thesis: contradiction
consider BE1 being Subset of (the_Edges_of G) such that
A3: for x being set holds
( x in BE1 iff ( x in the_Edges_of G & S<sub>1</sub>[x] ) ) from SUBSET_1:sch 1();
((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G by Th33;
then A4: ((PRIM:CompSeq G) . n) `1 c< G .reachableFrom the Element of the_Vertices_of G by A2, XBOOLE_0:def 8;

now :: thesis: not BE1 = {}

the Element of the_Vertices_of G in { the Element of the_Vertices_of G} by TARSKI:def 1;
then the Element of the_Vertices_of G in (PRIM:Init G) `1 ;
then A5: the Element of the_Vertices_of G in ((PRIM:CompSeq G) . 0) `1 by Def17;
assume A6: BE1 = {} ; :: thesis: contradiction
consider v being object such that
A7: v in G .reachableFrom the Element of the_Vertices_of G and
A8: not v in ((PRIM:CompSeq G) . n) `1 by A4, XBOOLE_0:6;
reconsider v = v as Vertex of G by A7;
consider W being Walk of G such that
A9: W is_Walk_from the Element of the_Vertices_of G,v by A7, GLIB_002:def 5;
defpred S<sub>2</sub>[ Nat] means ( $1 is odd & $1 <= len W & not W . $1 in ((PRIM:CompSeq G) . n) `1 );
W . (len W) = W .last() by GLIB_001:def 7
.= v by A9, GLIB_001:def 23 ;
then A10: ex k being Nat st S₂[k] by A8;
consider k being Nat such that
A11: ( S₂[k] & ( for m being Nat st S₂[m] holds
k <= m ) ) from NAT_1:sch 5(A10);
A12: ((PRIM:CompSeq G) . 0) `1 c= ((PRIM:CompSeq G) . n) `1 by Th34;

now :: thesis: contradiction

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: contradiction

then W . k = W .first() by GLIB_001:def 6
.= the Element of the_Vertices_of G by A9, GLIB_001:def 23 ;
hence contradiction by A5, A12, A11; :: thesis: verum

end;

suppose A13: k <> 1 ; :: thesis: contradiction

reconsider k9 = k as odd Element of NAT by A11, ORDINAL1:def 12;
1 <= k by A11, ABIAN:12;
then 1 < k by A13, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then reconsider k2a = k9 - (2 * 1) as odd Element of NAT by INT_1:5;
set e = W . (k2a + 1);
A14: k - 2 < (len W) - 0 by A11, XREAL_1:15;
then A15: W . (k2a + 1) Joins W . k2a,W . (k2a + 2),G by GLIB_001:def 3;
then A16: W . (k2a + 1) in the_Edges_of G ;
k2a < k - 0 by XREAL_1:15;
then A17: W . k2a in ((PRIM:CompSeq G) . n) `1 by A11, A14;
W . k in the_Vertices_of G by A15, GLIB_000:13;
then W . k in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) by A11, XBOOLE_0:def 5;
then S₁[W . (k2a + 1)] by A17, A15, GLIB_000:17;
hence contradiction by A3, A6, A16; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then reconsider BE1 = BE1 as non empty finite set ;
deffunc H₁( Element of BE1) -> set = (the_Weight_of G) . $1;
consider e1 being Element of BE1 such that
A18: for e2 being Element of BE1 holds H₁(e1) <= H₁(e2) from PRE_CIRC:sch 5();

A19: now :: thesis: for e2 being set st e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2

let e2 be set ; :: thesis: ( e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G implies (the_Weight_of G) . e1 <= (the_Weight_of G) . e2 )
assume A20: e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G ; :: thesis: (the_Weight_of G) . e1 <= (the_Weight_of G) . e2
reconsider e29 = e2 as Element of BE1 by A3, A20;
(the_Weight_of G) . e1 <= (the_Weight_of G) . e29 by A18;
hence (the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ; :: thesis: verum

end;

e1 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by A3;
hence contradiction by A1, A19, Def13; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum

end;

assume A21: ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G ; :: thesis: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {}

now :: thesis: not PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {}

assume PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: contradiction
then A22: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by Def13;
then A23: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in the_Edges_of G ;

now :: thesis: contradiction

per cases ( ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) ) or ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ) by A22;

suppose A24: ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) ) ; :: thesis: contradiction

A25: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) Joins (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),(the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),G by A23;
not (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 by A24, XBOOLE_0:def 5;
hence contradiction by A21, A24, A25, GLIB_002:10; :: thesis: verum

end;

suppose A26: ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: contradiction

A27: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) Joins (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),(the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n),G by A23;
not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 by A26, XBOOLE_0:def 5;
hence contradiction by A21, A26, A27, GLIB_002:10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: verum