let S1, S2 be Graph-membered set ; :: thesis:
( (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) & (the_Vertices_of S2) \ (the_Vertices_of S1) c= the_Vertices_of (S2 \ S1) ) by Th10;
then (the_Vertices_of S1) \+\ (the_Vertices_of S2) c= (the_Vertices_of (S1 \ S2)) \/ (the_Vertices_of (S2 \ S1)) by XBOOLE_1:13;
hence (the_Vertices_of S1) \+\ (the_Vertices_of S2) c= the_Vertices_of (S1 \+\ S2) by Th8; :: thesis:
( (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) & (the_Edges_of S2) \ (the_Edges_of S1) c= the_Edges_of (S2 \ S1) ) by Th10;
then (the_Edges_of S1) \+\ (the_Edges_of S2) c= (the_Edges_of (S1 \ S2)) \/ (the_Edges_of (S2 \ S1)) by XBOOLE_1:13;
hence (the_Edges_of S1) \+\ (the_Edges_of S2) c= the_Edges_of (S1 \+\ S2) by Th8; :: thesis:
( (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) & (the_Source_of S2) \ (the_Source_of S1) c= the_Source_of (S2 \ S1) ) by Th10;
then (the_Source_of S1) \+\ (the_Source_of S2) c= (the_Source_of (S1 \ S2)) \/ (the_Source_of (S2 \ S1)) by XBOOLE_1:13;
hence (the_Source_of S1) \+\ (the_Source_of S2) c= the_Source_of (S1 \+\ S2) by Th8; :: thesis:
( (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) & (the_Target_of S2) \ (the_Target_of S1) c= the_Target_of (S2 \ S1) ) by Th10;
then (the_Target_of S1) \+\ (the_Target_of S2) c= (the_Target_of (S1 \ S2)) \/ (the_Target_of (S2 \ S1)) by XBOOLE_1:13;
hence (the_Target_of S1) \+\ (the_Target_of S2) c= the_Target_of (S1 \+\ S2) by Th8; :: thesis: