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 )
the_Vertices_of (createGraph {1},{} ,S,S) = {1} by FINSEQ_4:91;
then card (the_Vertices_of (createGraph {1},{} ,S,S)) = 1 by CARD_1:50;
hence createGraph {1},{} ,S,S is trivial by Def21; :: thesis: createGraph {1},{} ,S,S is simple
the_Edges_of (createGraph {1},{} ,S,S) = {} by FINSEQ_4:91;
then 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 Def15;
then A1: createGraph {1},{} ,S,S is non-multi by Def22;
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 createGraph {1},{} ,S,S is loopless by Def20;
hence createGraph {1},{} ,S,S is simple by A1; :: thesis: verum