let S1, S2 be Graph-membered set ; :: thesis:
assume A1: S1 c= S2 ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in the_Vertices_of S1 ; :: thesis:
then consider G being _Graph such that
A2: ( G in S1 & x = the_Vertices_of G ) by GLIB_014:def 14;
thus x in the_Vertices_of S2 by A1, A2, GLIB_014:def 14; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in the_Edges_of S1 ; :: thesis:
then consider G being _Graph such that
A3: ( G in S1 & x = the_Edges_of G ) by GLIB_014:def 15;
thus x in the_Edges_of S2 by A1, A3, GLIB_014:def 15; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in the_Source_of S1 ; :: thesis:
then consider G being _Graph such that
A4: ( G in S1 & x = the_Source_of G ) by GLIB_014:def 16;
thus x in the_Source_of S2 by A1, A4, GLIB_014:def 16; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in the_Target_of S1 ; :: thesis:
then consider G being _Graph such that
A5: ( G in S1 & x = the_Target_of G ) by GLIB_014:def 17;
thus x in the_Target_of S2 by A1, A5, GLIB_014:def 17; :: thesis:

end;

hence the_Target_of S1 c= the_Target_of S2 by TARSKI:def 3; :: thesis:
thus verum ; :: thesis: