set V5 = {1};
set E3 = {} ;
consider S1 being Function of {},{1};
consider W1 being ManySortedSet of {} ;
consider EL8 being PartFunc of {},REAL;
consider VL6 being PartFunc of {1},REAL;
set G = (((((<*{1}*> ^ <*{}*>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>;
A1:
dom VL6 c= {1}
;
A2:
len ((((((<*{1}*> ^ <*{}*>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) = 7
by FINSEQ_1:90;
then
dom ((((((<*{1}*> ^ <*{}*>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>) = Seg 7
by FINSEQ_1:def 3;
then reconsider G = (((((<*{1}*> ^ <*{}*>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*> as GraphStruct by RELAT_1:def 18;
A3:
dom G = Seg 7
by A2, FINSEQ_1:def 3;
then A4:
( SourceSelector in dom G & TargetSelector in dom G )
by FINSEQ_1:3;
A5:
( WeightSelector in dom G & ELabelSelector in dom G )
by A3, FINSEQ_1:3;
A6:
( G . WeightSelector = W1 & G . ELabelSelector = EL8 )
by FINSEQ_1:90;
take
G
; ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] )
A7:
( the_Vertices_of G = {1} & the_Edges_of G = {} )
by FINSEQ_1:90;
A8:
( the_Source_of G = S1 & the_Target_of G = S1 )
by FINSEQ_1:90;
A9:
VLabelSelector in dom G
by A3, FINSEQ_1:3;
A10:
( G . VLabelSelector = VL6 & dom EL8 c= {} )
by FINSEQ_1:90;
( VertexSelector in dom G & EdgeSelector in dom G )
by A3, FINSEQ_1:3;
hence
( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] )
by A4, A5, A9, A7, A8, A6, A10, A1, Def4, Def5, Def6, GLIB_000:def 11; verum