let S1, S2 be Graph-membered set ; :: thesis: ( S1 c= S2 implies ( the_Vertices_of S1 c= the_Vertices_of S2 & the_Edges_of S1 c= the_Edges_of S2 & the_Source_of S1 c= the_Source_of S2 & the_Target_of S1 c= the_Target_of S2 ) )
assume A1: S1 c= S2 ; :: thesis: ( the_Vertices_of S1 c= the_Vertices_of S2 & the_Edges_of S1 c= the_Edges_of S2 & the_Source_of S1 c= the_Source_of S2 & the_Target_of S1 c= the_Target_of S2 )

now :: thesis: for x being object st x in the_Vertices_of S1 holds
x in the_Vertices_of S2

let x be object ; :: thesis: ( x in the_Vertices_of S1 implies x in the_Vertices_of S2 )
assume x in the_Vertices_of S1 ; :: thesis: x in the_Vertices_of S2
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: verum

end;

hence the_Vertices_of S1 c= the_Vertices_of S2 by TARSKI:def 3; :: thesis: ( the_Edges_of S1 c= the_Edges_of S2 & the_Source_of S1 c= the_Source_of S2 & the_Target_of S1 c= the_Target_of S2 )

now :: thesis: for x being object st x in the_Edges_of S1 holds
x in the_Edges_of S2

let x be object ; :: thesis: ( x in the_Edges_of S1 implies x in the_Edges_of S2 )
assume x in the_Edges_of S1 ; :: thesis: x in the_Edges_of S2
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: verum

end;

hence the_Edges_of S1 c= the_Edges_of S2 by TARSKI:def 3; :: thesis: ( the_Source_of S1 c= the_Source_of S2 & the_Target_of S1 c= the_Target_of S2 )

now :: thesis: for x being object st x in the_Source_of S1 holds
x in the_Source_of S2

let x be object ; :: thesis: ( x in the_Source_of S1 implies x in the_Source_of S2 )
assume x in the_Source_of S1 ; :: thesis: x in the_Source_of S2
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: verum

end;

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

now :: thesis: for x being object st x in the_Target_of S1 holds
x in the_Target_of S2

let x be object ; :: thesis: ( x in the_Target_of S1 implies x in the_Target_of S2 )
assume x in the_Target_of S1 ; :: thesis: x in the_Target_of S2
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: verum

end;

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