consider G1 being finite non trivial Tree-like _Graph;
set W = (the_Edges_of G1) --> 0 ;
A4: ( dom ((the_Edges_of G1) --> 0 ) = the_Edges_of G1 & rng ((the_Edges_of G1) --> 0 ) c= {0 } ) by FUNCOP_1:19;
then reconsider W = (the_Edges_of G1) --> 0 as Function of (the_Edges_of G1),REAL by FUNCT_2:4;
set G2 = G1 .set WeightSelector ,W;
reconsider EL = {} as PartFunc of (the_Edges_of (G1 .set WeightSelector ,W)),REAL by RELSET_1:25;
set G3 = (G1 .set WeightSelector ,W) .set ELabelSelector ,EL;
reconsider VL = {} as PartFunc of (the_Vertices_of ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL)),REAL by RELSET_1:25;
set G4 = ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL;
take ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL ; :: thesis: ( ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is finite & not ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is trivial & ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is Tree-like & ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted & ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV )
thus ( ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is finite & not ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is trivial & ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is Tree-like ) ; :: thesis: ( ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted & ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV )
A5: the_Weight_of (((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL) = ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) . WeightSelector by GLIB_000:12
.= (G1 .set WeightSelector ,W) . WeightSelector by GLIB_000:12
.= W by GLIB_000:11 ;
then A6: ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-weighted by Def13;
the_ELabel_of (((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL) = ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) . ELabelSelector by GLIB_000:12
.= EL by GLIB_000:11 ;
then A7: ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-elabeled by Def15;

now

let x be set ; :: thesis: ( x in {0 } implies x in Real>=0 )
assume x in {0 } ; :: thesis: x in Real>=0
then x = 0 by TARSKI:def 1;
hence x in Real>=0 by GRAPH_5:def 12; :: thesis: verum

end;

then {0 } c= Real>=0 by TARSKI:def 3;
then rng W c= Real>=0 by A4, XBOOLE_1:1;
hence ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted by A5, Def14; :: thesis: ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV
thus ((G1 .set WeightSelector ,W) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV by A6, A7; :: thesis: verum