set V = {1};
set E = {} ;
reconsider S = {} as Function of {},{1} by RELSET_1:12;
set G = <*{1},{},S,S*>;
len <*{1},{},S,S*> = 4 by FINSEQ_4:76;
then A1: dom <*{1},{},S,S*> = Seg 4 by FINSEQ_1:def 3;
then reconsider G = <*{1},{},S,S*> as GraphStruct by RELAT_1:def 18;
A2: ( SourceSelector in dom G & TargetSelector in dom G ) by A1, FINSEQ_1:1;
A3: ( the_Vertices_of G = {1} & the_Edges_of G = {} ) by FINSEQ_4:76;
A4: ( the_Source_of G = S & the_Target_of G = S ) by FINSEQ_4:76;
( VertexSelector in dom G & EdgeSelector in dom G ) by A1, FINSEQ_1:1;
then G is [Graph-like] by A3, A4, A2, Def11;
hence ex b₁ being GraphStruct st b₁ is [Graph-like] ; :: thesis: verum