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))),NAT;
set G2 = (createGraph ({1},{},S,S)) .set (WeightSelector,WL);
take (createGraph ({1},{},S,S)) .set (WeightSelector,WL) ; :: thesis: ( (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is finite & (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is trivial & (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is Tree-like & (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is natural-weighted )
thus ( (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is finite & (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is trivial & (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is Tree-like ) ; :: thesis: (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is natural-weighted
the_Weight_of ((createGraph ({1},{},S,S)) .set (WeightSelector,WL)) = WL by GLIB_000:11;
hence (createGraph ({1},{},S,S)) .set (WeightSelector,WL) is natural-weighted by Def1; :: thesis: verum