for S1, S2 being Graph-membered set holds
( (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) & (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) & (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) & (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) )