consider GT being spanning Tree-like WSubgraph of spanning Tree-like ;
set G3 = GT .strict WGraphSelectors ;
A1: GT .strict WGraphSelectors == GT by Lm4;
the_Weight_of (GT .strict WGraphSelectors ) = the_Weight_of GT by Lm4;
then reconsider G3 = GT .strict WGraphSelectors as WSubgraph of by A1, GLIB_003:15;
the_Vertices_of G3 = the_Vertices_of GT by A1, GLIB_000:def 36
.= the_Vertices_of G1 by GLIB_000:def 35 ;
then reconsider G3 = G3 as spanning Tree-like WSubgraph of spanning Tree-like by A1, GLIB_000:def 35, GLIB_002:48;
set X = { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of spanning Tree-like } ;

now

let x be set ; :: thesis: ( x in { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of spanning Tree-like } implies x in G1 .allWSubgraphs() )
assume x in { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of spanning Tree-like } ; :: thesis: x in G1 .allWSubgraphs()
then ex G2 being Element of G1 .allWSubgraphs() st
( x = G2 & G2 is spanning Tree-like WSubgraph of spanning Tree-like ) ;
hence x in G1 .allWSubgraphs() ; :: thesis: verum

end;

then reconsider X = { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of spanning Tree-like } as finite Subset of by TARSKI:def 3;
deffunc H₁( finite real-weighted WGraph) -> Real = G1 .cost() ;
dom G3 = WGraphSelectors by Lm5;
then G3 in G1 .allWSubgraphs() by Def5;
then G3 in X ;
then reconsider X = X as non empty finite Subset of ;
consider x being Element of X such that
A2: for y being Element of X holds H₁(x) <= H₁(y) from GRAPH_5:sch 2();
x in X ;
then ex G2 being Element of G1 .allWSubgraphs() st
( x = G2 & G2 is spanning Tree-like WSubgraph of spanning Tree-like ) ;
then reconsider x = x as spanning Tree-like WSubgraph of spanning Tree-like ;
take x ; :: thesis: x is min-cost

now

let GT be spanning Tree-like WSubgraph of spanning Tree-like ; :: thesis: x .cost() <= GT .cost()
set G3 = GT .strict WGraphSelectors ;
A3: GT .strict WGraphSelectors == GT by Lm4;
A4: the_Weight_of (GT .strict WGraphSelectors ) = the_Weight_of GT by Lm4;
then reconsider G3 = GT .strict WGraphSelectors as WSubgraph of by A3, GLIB_003:15;
the_Vertices_of G3 = the_Vertices_of GT by A3, GLIB_000:def 36
.= the_Vertices_of G1 by GLIB_000:def 35 ;
then reconsider G3 = G3 as spanning Tree-like WSubgraph of spanning Tree-like by A3, GLIB_000:def 35, GLIB_002:48;
dom G3 = WGraphSelectors by Lm5;
then G3 in G1 .allWSubgraphs() by Def5;
then G3 in X ;
then x .cost() <= G3 .cost() by A2;
hence x .cost() <= GT .cost() by A3, A4, GLIB_000:def 36; :: thesis: verum

end;

hence x is min-cost by Def19; :: thesis: verum