set E = {} ;
set V = {1};
reconsider S = {} as Function of {},{1} by RELSET_1:12;
set G1 = createGraph ({1},{},S,S);
set WL = the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT;
set G2 = (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT);
take
(createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT)
; ( (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is _finite & (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is _trivial & (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is Tree-like & (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is natural-weighted )
thus
( (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is _finite & (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is _trivial & (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is Tree-like )
; (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is natural-weighted
the_Weight_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT)) = the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT
by GLIB_000:8;
hence
(createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),NAT) is natural-weighted
; verum