set GT = the spanning Tree-like WSubgraph of G1;
set G3 = the spanning Tree-like WSubgraph of G1 | WGraphSelectors;
A1: the spanning Tree-like WSubgraph of G1 | WGraphSelectors == the spanning Tree-like WSubgraph of G1 by Lm4;
the_Weight_of ( the spanning Tree-like WSubgraph of G1 | WGraphSelectors) = the_Weight_of the spanning Tree-like WSubgraph of G1 by Lm4;
then reconsider G3 = the spanning Tree-like WSubgraph of G1 | WGraphSelectors as WSubgraph of G1 by A1, GLIB_003:8;
the_Vertices_of G3 = the_Vertices_of the spanning Tree-like WSubgraph of G1 by A1
.= the_Vertices_of G1 by GLIB_000:def 33 ;
then reconsider G3 = G3 as spanning Tree-like WSubgraph of G1 by A1, GLIB_000:def 33, GLIB_002:48;
set X = { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of G1 } ;

now :: thesis: for x being object st x in { G2 where G2 is Element of G1 .allWSubgraphs() : G2 is spanning Tree-like WSubgraph of G1 } holds
x in G1 .allWSubgraphs()

let x be object ; :: 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 PRE_CIRC:sch 5();
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 :: thesis: for GT being spanning Tree-like WSubgraph of G1 holds x .cost() <= GT .cost()

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:8;
the_Vertices_of G3 = the_Vertices_of GT by A3
.= the_Vertices_of G1 by GLIB_000:def 33 ;
then reconsider G3 = G3 as spanning Tree-like WSubgraph of G1 by A3, GLIB_000:def 33, 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; :: thesis: verum

end;

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