set V = {1};
set E = {} ;
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 Def3; :: thesis: verum