consider GT being spanning Tree-like WSubgraph of G1;
set G3 = GT | WGraphSelectors ;
A1: GT | WGraphSelectors == GT by Lm4;
the_Weight_of (GT | WGraphSelectors ) = the_Weight_of GT by Lm4;
then reconsider G3 = GT | WGraphSelectors as WSubgraph of G1 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 G1 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 G1 } ;

now

let x be set ; :: thesis: ( x in { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of G1 } implies x in G1 .allWSubgraphs() )
assume x in { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of G1 } ; :: thesis: x in G1 .allWSubgraphs()
then ex G2 being Element of G1 .allWSubgraphs() st
( x = G2 & G2 is spanning Tree-like WSubgraph of G1 ) ;
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 G1 } as finite Subset of (G1 .allWSubgraphs() ) 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 (G1 .allWSubgraphs() ) ;
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 G1 ) ;
then reconsider x = x as spanning Tree-like WSubgraph of G1 ;
take x ; :: thesis: x is min-cost

now

let GT be spanning Tree-like WSubgraph of G1; :: thesis: x .cost() <= GT .cost()
set G3 = GT | WGraphSelectors ;
A3: GT | WGraphSelectors == GT by Lm4;
A4: the_Weight_of (GT | WGraphSelectors ) = the_Weight_of GT by Lm4;
then reconsider G3 = GT | WGraphSelectors as WSubgraph of G1 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 G1 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