set G = <*V,E,S,T*>;
len <*V,E,S,T*> = 4
by FINSEQ_4:76;
then A1:
dom <*V,E,S,T*> = Seg 4
by FINSEQ_1:def 3;
reconsider G = <*V,E,S,T*> as GraphStruct ;
A2:
( SourceSelector in dom G & TargetSelector in dom G )
by A1, FINSEQ_1:1;
A3:
( the_Vertices_of G = V & the_Edges_of G = E )
by FINSEQ_4:76;
A4:
( the_Source_of G = S & the_Target_of G = T )
by FINSEQ_4:76;
( VertexSelector in dom G & EdgeSelector in dom G )
by A1, FINSEQ_1:1;
hence
<*V,E,S,T*> is _Graph
by A3, A4, A2, Def10; verum