let G1, G2 be finite connected real-weighted WGraph; :: thesis: for G3 being WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G3 is minimumSpanningTree of G2
let G3 be WSubgraph of G1; :: thesis: ( G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 implies G3 is minimumSpanningTree of G2 )
assume A1: ( G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 ) ; :: thesis: G3 is minimumSpanningTree of G2
set G3' = G3;
reconsider G3' = G3 as Tree-like WSubgraph of G2 by A1, GLIB_003:17;
the_Vertices_of G3 = the_Vertices_of G1 by A1, GLIB_000:def 35
.= the_Vertices_of G2 by A1, GLIB_000:def 36 ;
then reconsider G3' = G3' as spanning Tree-like WSubgraph of G2 by GLIB_000:def 35;

now

let G be spanning Tree-like WSubgraph of G2; :: thesis: G3 .cost() <= G .cost()
reconsider G' = G as Tree-like WSubgraph of G1 by A1, GLIB_003:17;
the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 35
.= the_Vertices_of G1 by A1, GLIB_000:def 36 ;
then G' is spanning by GLIB_000:def 35;
hence G3 .cost() <= G .cost() by A1, Def17; :: thesis: verum

end;

then G3' is min-cost by Def17;
hence G3 is minimumSpanningTree of G2 ; :: thesis: verum