let GS be GraphStruct; :: thesis: ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of the_Edges_of GS, the_Vertices_of GS & the_Target_of GS is Function of the_Edges_of GS, the_Vertices_of GS ) )

now

hereby :: thesis: ( _GraphSelectors c= dom GS implies ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) )

assume ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) ; :: thesis: _GraphSelectors c= dom GS
then for x being set st x in _GraphSelectors holds
x in dom GS by ENUMSET1:def 2;
hence _GraphSelectors c= dom GS by TARSKI:def 3; :: thesis: verum

end;

A1: ( VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors ) by ENUMSET1:def 2;
A2: ( SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors ) by ENUMSET1:def 2;
assume _GraphSelectors c= dom GS ; :: thesis: ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS )
hence ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) by A1, A2; :: thesis: verum

end;

hence ( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of the_Edges_of GS, the_Vertices_of GS & the_Target_of GS is Function of the_Edges_of GS, the_Vertices_of GS ) ) by Def11; :: thesis: verum