set V5 = {1};
set E3 = {} ;
set S1 = the Function of {},{1};
set W1 = the ManySortedSet of {} ;
set EL8 = the PartFunc of {},REAL;
set VL6 = the PartFunc of {1},REAL;
set G = (((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*>;
A1: dom the PartFunc of {1},REAL c= {1} ;
A2: len ((((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*>) = 7 by FINSEQ_1:69;
reconsider G = (((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*> as GraphStruct ;
A3: dom G = Seg 7 by A2, FINSEQ_1:def 3;
then A4: ( SourceSelector in dom G & TargetSelector in dom G ) by FINSEQ_1:1;
A5: ( WeightSelector in dom G & ELabelSelector in dom G ) by A3, FINSEQ_1:1;
A6: ( G . WeightSelector = the ManySortedSet of {} & G . ELabelSelector = the PartFunc of {},REAL ) by FINSEQ_1:69;
take G ; :: thesis: ( 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:69;
A8: ( the_Source_of G = the Function of {},{1} & the_Target_of G = the Function of {},{1} ) by FINSEQ_1:69;
A9: VLabelSelector in dom G by A3, FINSEQ_1:1;
A10: ( G . VLabelSelector = the PartFunc of {1},REAL & dom the PartFunc of {},REAL c= {} ) by FINSEQ_1:69;
( VertexSelector in dom G & EdgeSelector in dom G ) by A3, FINSEQ_1:1;
hence ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] ) by A4, A5, A9, A7, A8, A6, A10, A1; :: thesis: verum