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 that
A1: G3 is minimumSpanningTree of G1 and
A2: G1 == G2 and
A3: the_Weight_of G1 = the_Weight_of G2 ; :: thesis: G3 is minimumSpanningTree of G2
set G39 = G3;
reconsider G39 = G3 as Tree-like WSubgraph of G2 by A1, A2, A3, GLIB_003:10;
the_Vertices_of G3 = the_Vertices_of G1 by A1, GLIB_000:def 33
.= the_Vertices_of G2 by A2, GLIB_000:def 34 ;
then reconsider G39 = G39 as spanning Tree-like WSubgraph of G2 by GLIB_000:def 33;

now

let G be spanning Tree-like WSubgraph of G2; :: thesis: G3 .cost() <= G .cost()
reconsider G9 = G as Tree-like WSubgraph of G1 by A2, A3, GLIB_003:10;
the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 33
.= the_Vertices_of G1 by A2, GLIB_000:def 34 ;
then G9 is spanning by GLIB_000:def 33;
hence G3 .cost() <= G .cost() by A1, Def19; :: thesis: verum

end;

then G39 is min-cost by Def19;
hence G3 is minimumSpanningTree of G2 ; :: thesis: verum