set V = {1};
set E = {} ;
reconsider S = {} as Function of {} ,{1} by RELSET_1:25;
set G = createGraph {1},{} ,S,S;
take createGraph {1},{} ,S,S ; :: thesis: ( createGraph {1},{} ,S,S is trivial & createGraph {1},{} ,S,S is simple )
A1: ( the_Vertices_of (createGraph {1},{} ,S,S) = {1} & the_Edges_of (createGraph {1},{} ,S,S) = {} ) by FINSEQ_4:91;
for e being set holds
( not e in the_Edges_of (createGraph {1},{} ,S,S) or not (the_Source_of (createGraph {1},{} ,S,S)) . e = (the_Target_of (createGraph {1},{} ,S,S)) . e ) by FINSEQ_4:91;
then A2: createGraph {1},{} ,S,S is loopless by Def20;
card (the_Vertices_of (createGraph {1},{} ,S,S)) = 1 by A1, CARD_1:50;
hence createGraph {1},{} ,S,S is trivial by Def21; :: thesis: createGraph {1},{} ,S,S is simple
for e1, e2, v1, v2 being set st e1 Joins v1,v2, createGraph {1},{} ,S,S & e2 Joins v1,v2, createGraph {1},{} ,S,S holds
e1 = e2 by A1, Def15;
then createGraph {1},{} ,S,S is non-multi by Def22;
hence createGraph {1},{} ,S,S is simple by A2; :: thesis: verum