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
; ( IT is _trivial & IT is simple )
thus
( IT is _trivial & IT is simple )
; verum