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