set E = {} ;
set V = {1};
reconsider S = {} as Function of {} ,{1} by RELSET_1:25;
set G1 = createGraph {1},{} ,S,S;
consider WL being Function of (the_Edges_of (createGraph {1},{} ,S,S)),REAL ;
set G2 = (createGraph {1},{} ,S,S) .set WeightSelector ,WL;
consider EL being PartFunc of (the_Edges_of ((createGraph {1},{} ,S,S) .set WeightSelector ,WL)),REAL ;
set G3 = ((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL;
consider VL being PartFunc of (the_Vertices_of (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL)),REAL ;
set G4 = (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL;
take (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL ; :: thesis: ( (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is finite & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is trivial & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is Tree-like & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV )
thus ( (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is finite & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is trivial & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is Tree-like ) ; :: thesis: ( (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted & (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV )
A1: the_Weight_of ((((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL) = (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) . WeightSelector by GLIB_000:12
.= ((createGraph {1},{} ,S,S) .set WeightSelector ,WL) . WeightSelector by GLIB_000:12
.= WL by GLIB_000:11 ;
the_Edges_of (createGraph {1},{} ,S,S) = {} by GLIB_000:8;
then rng (the_Weight_of ((((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL)) = {} by A1;
then rng (the_Weight_of ((((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL)) c= Real>=0 by XBOOLE_1:2;
hence (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is nonnegative-weighted by Def14; :: thesis: (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV
the_ELabel_of ((((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL) = (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) . ELabelSelector by GLIB_000:12
.= EL by GLIB_000:11 ;
then A2: (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-elabeled by Def15;
(((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-weighted by A1, Def13;
hence (((createGraph {1},{} ,S,S) .set WeightSelector ,WL) .set ELabelSelector ,EL) .set VLabelSelector ,VL is real-WEV by A2; :: thesis: verum