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;
( the_Vertices_of (createGraph {v},{} ,S,S) = {v} & the_Edges_of (createGraph {v},{} ,S,S) = {} ) by FINSEQ_4:91;
then A1: ( the_Vertices_of (createGraph {v},{} ,S,S) c= the_Vertices_of G & the_Edges_of (createGraph {v},{} ,S,S) c= the_Edges_of G ) by XBOOLE_1:2;
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;
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