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))),REAL;
set G2 = (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL);
set EL = the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL;
set G3 = ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL);
set VL = the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL;
set G4 = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL);
take (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) ; :: thesis: ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is _finite & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is _trivial & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is Tree-like & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV )
thus ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is _finite & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is _trivial & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is Tree-like ) ; :: thesis: ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV )
A1: the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL)) = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) . WeightSelector by GLIB_000:9
.= ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) . WeightSelector by GLIB_000:9
.= the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL by GLIB_000:8 ;
rng (the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL))) = {} by A1;
then rng (the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL))) c= Real>=0 by XBOOLE_1:2;
hence (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted ; :: thesis: (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV
the_ELabel_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL)) = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) . ELabelSelector by GLIB_000:9
.= the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL by GLIB_000:8 ;
then A2: (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-elabeled ;
(((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-weighted by A1;
hence (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV by A2; :: thesis: verum