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