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