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;
reconsider G = <*{1},{},S,S*> as GraphStruct ;
A2: ( SourceSelector in dom G & TargetSelector in dom G ) by A1, FINSEQ_1:1;
( VertexSelector in dom G & EdgeSelector in dom G ) by A1, FINSEQ_1:1;
then G is [Graph-like] by A2;
hence ex b₁ being GraphStruct st b₁ is [Graph-like] ; :: thesis: verum