set G1 = the finite non trivial Tree-like _Graph;
set W = (the_Edges_of the finite non trivial Tree-like _Graph) --> 0;
A3: dom ((the_Edges_of the finite non trivial Tree-like _Graph) --> 0) = the_Edges_of the finite non trivial Tree-like _Graph by FUNCOP_1:13;
A4: rng ((the_Edges_of the finite non trivial Tree-like _Graph) --> 0) c= {0} by FUNCOP_1:13;
then reconsider W = (the_Edges_of the finite non trivial Tree-like _Graph) --> 0 as Function of (the_Edges_of the finite non trivial Tree-like _Graph),REAL by A3, FUNCT_2:2;
set G2 = the finite non trivial Tree-like _Graph .set (WeightSelector,W);
reconsider EL = {} as PartFunc of (the_Edges_of ( the finite non trivial Tree-like _Graph .set (WeightSelector,W))),REAL by RELSET_1:12;
set G3 = ( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL);
reconsider VL = {} as PartFunc of (the_Vertices_of (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL))),REAL by RELSET_1:12;
set G4 = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL);
take (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) ; :: thesis: ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is finite & not (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is trivial & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is Tree-like & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV )
thus ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is finite & not (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is trivial & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is Tree-like ) ; :: thesis: ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV )
A5: the_Weight_of ((( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL)) = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) . WeightSelector by GLIB_000:9
.= ( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) . WeightSelector by GLIB_000:9
.= W by GLIB_000:8 ;

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 (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted by A5, Def14; :: thesis: (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV
the_ELabel_of ((( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL)) = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) . ELabelSelector by GLIB_000:9
.= EL by GLIB_000:8 ;
then A6: (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-elabeled by Def15;
(( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-weighted by A5, Def13;
hence (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV by A6; :: thesis: verum