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 :: thesis: ( ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS implies _GraphSelectors c= dom GS ) & ( _GraphSelectors c= dom GS implies ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) ) )
thus ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS implies _GraphSelectors c= dom GS ) by ENUMSET1:def 2; :: thesis: ( _GraphSelectors c= dom GS implies ( VertexSelector in dom GS & EdgeSelector in dom GS & SourceSelector in dom GS & TargetSelector in dom GS ) )
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) ) ) ; :: thesis: verum