consider v being Element of the_Vertices_of G;
set V = {v};
set E = {} ;
reconsider S = {} as Function of {},{v} by RELSET_1:25;
set IT = createGraph ({v},{},S,S);
A1: ( the_Vertices_of (createGraph ({v},{},S,S)) = {v} & ( for e being set st e in the_Edges_of (createGraph ({v},{},S,S)) holds
( (the_Source_of (createGraph ({v},{},S,S))) . e = (the_Source_of G) . e & (the_Target_of (createGraph ({v},{},S,S))) . e = (the_Target_of G) . e ) ) ) by FINSEQ_4:91;
the_Edges_of (createGraph ({v},{},S,S)) = {} by FINSEQ_4:91;
then the_Edges_of (createGraph ({v},{},S,S)) c= the_Edges_of G by XBOOLE_1:2;
then reconsider IT = createGraph ({v},{},S,S) as Subgraph of G by A1, Def34;
take IT ; :: thesis: ( IT is trivial & IT is simple )
thus ( IT is trivial & IT is simple ) ; :: thesis: verum