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