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 ;
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 ;
for x being object st x in {0} holds
x in Real>=0 by GRAPH_5:def 12;
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; :: 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 ;
(( the _finite non _trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-weighted by A5;
hence (( the _finite non _trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV by A6; :: thesis: verum