set v = the Element of the_Vertices_of G;
set V = { the Element of the_Vertices_of G};
set E = {} ;
reconsider S = {} as Function of {},{ the Element of the_Vertices_of G} by RELSET_1:12;
set IT = createGraph ({ the Element of the_Vertices_of G},{},S,S);
A1: ( the_Vertices_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) = { the Element of the_Vertices_of G} & ( for e being set st e in the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) holds
( (the_Source_of (createGraph ({ the Element of the_Vertices_of G},{},S,S))) . e = (the_Source_of G) . e & (the_Target_of (createGraph ({ the Element of the_Vertices_of G},{},S,S))) . e = (the_Target_of G) . e ) ) ) by FINSEQ_4:76;
the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) = {} by FINSEQ_4:76;
then the_Edges_of (createGraph ({ the Element of the_Vertices_of G},{},S,S)) c= the_Edges_of G ;
then reconsider IT = createGraph ({ the Element of the_Vertices_of G},{},S,S) as Subgraph of G by A1, Def32;
take IT ; :: thesis: ( IT is _trivial & IT is simple )
thus ( IT is _trivial & IT is simple ) ; :: thesis: verum