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