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; :: thesis: verum