let G be _finite connected real-weighted WGraph; :: thesis: for G1 being minimumSpanningTree of G
for G2 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G2 is minimumSpanningTree of G
let G1 be minimumSpanningTree of G; :: thesis: for G2 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G2 is minimumSpanningTree of G
let G2 be WGraph; :: thesis: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 implies G2 is minimumSpanningTree of G )
assume that
A1: G1 == G2 and
A2: the_Weight_of G1 = the_Weight_of G2 ; :: thesis: G2 is minimumSpanningTree of G
reconsider G29 = G2 as WSubgraph of G by A1, A2, GLIB_003:8;
the_Vertices_of G2 = the_Vertices_of G1 by A1
.= the_Vertices_of G by GLIB_000:def 33 ;
then reconsider G29 = G29 as spanning Tree-like WSubgraph of G by A1, GLIB_000:def 33, GLIB_002:48;

now :: thesis: for G3 being spanning Tree-like WSubgraph of G holds G29 .cost() <= G3 .cost()

let G3 be spanning Tree-like WSubgraph of G; :: thesis: G29 .cost() <= G3 .cost()
G1 .cost() <= G3 .cost() by Def19;
hence G29 .cost() <= G3 .cost() by A1, A2; :: thesis: verum

end;

hence G2 is minimumSpanningTree of G by Def19; :: thesis: verum