reconsider V1 = (the_Vertices_of G) \/ V as non empty set ;
A1: the_Vertices_of G c= V1 by XBOOLE_1:7;
set E = the_Edges_of G;
reconsider S1 = the_Source_of G as Function of (the_Edges_of G),V1 by A1, FUNCT_2:7;
reconsider T1 = the_Target_of G as Function of (the_Edges_of G),V1 by A1, FUNCT_2:7;
set G1 = createGraph (V1,(the_Edges_of G),S1,T1);
for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of (createGraph (V1,(the_Edges_of G),S1,T1))) . e & (the_Target_of G) . e = (the_Target_of (createGraph (V1,(the_Edges_of G),S1,T1))) . e ) ;
then reconsider G1 = createGraph (V1,(the_Edges_of G),S1,T1) as Supergraph of G by Def9, XBOOLE_1:7;
take G1 ; :: thesis: ( the_Vertices_of G1 = (the_Vertices_of G) \/ V & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = the_Source_of G & the_Target_of G1 = the_Target_of G )
thus ( the_Vertices_of G1 = (the_Vertices_of G) \/ V & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = the_Source_of G & the_Target_of G1 = the_Target_of G ) ; :: thesis: verum