let S1, S2 be Graph-membered set ; :: thesis:

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in (the_Vertices_of S1) \ (the_Vertices_of S2) ; :: thesis:
then A1: ( x in the_Vertices_of S1 & not x in the_Vertices_of S2 ) by XBOOLE_0:def 5;
then consider G being _Graph such that
A2: ( G in S1 & x = the_Vertices_of G ) by Def14;
not G in S2 by A1, A2, Def14;
then G in S1 \ S2 by A2, XBOOLE_0:def 5;
hence x in the_Vertices_of (S1 \ S2) by A2, Def14; :: thesis:

end;

hence (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) by TARSKI:def 3; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in (the_Edges_of S1) \ (the_Edges_of S2) ; :: thesis:
then A3: ( x in the_Edges_of S1 & not x in the_Edges_of S2 ) by XBOOLE_0:def 5;
then consider G being _Graph such that
A4: ( G in S1 & x = the_Edges_of G ) by Def15;
not G in S2 by A3, A4, Def15;
then G in S1 \ S2 by A4, XBOOLE_0:def 5;
hence x in the_Edges_of (S1 \ S2) by A4, Def15; :: thesis:

end;

hence (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) by TARSKI:def 3; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in (the_Source_of S1) \ (the_Source_of S2) ; :: thesis:
then A5: ( x in the_Source_of S1 & not x in the_Source_of S2 ) by XBOOLE_0:def 5;
then consider G being _Graph such that
A6: ( G in S1 & x = the_Source_of G ) by Def16;
not G in S2 by A5, A6, Def16;
then G in S1 \ S2 by A6, XBOOLE_0:def 5;
hence x in the_Source_of (S1 \ S2) by A6, Def16; :: thesis:

end;

hence (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) by TARSKI:def 3; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in (the_Target_of S1) \ (the_Target_of S2) ; :: thesis:
then A7: ( x in the_Target_of S1 & not x in the_Target_of S2 ) by XBOOLE_0:def 5;
then consider G being _Graph such that
A8: ( G in S1 & x = the_Target_of G ) by Def17;
not G in S2 by A7, A8, Def17;
then G in S1 \ S2 by A8, XBOOLE_0:def 5;
hence x in the_Target_of (S1 \ S2) by A8, Def17; :: thesis:

end;

hence (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) by TARSKI:def 3; :: thesis:

end;