set V = {1,2};
set E = {} ;
reconsider S = {} as Function of {},{1,2} by RELSET_1:12;
set G = createGraph ({1,2},{},S,S);
take
createGraph ({1,2},{},S,S)
; ( 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:76;
A3:
the_Vertices_of (createGraph ({1,2},{},S,S)) = {1,2}
by FINSEQ_4:76;
hence
createGraph ({1,2},{},S,S) is _finite
by A2; ( 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:57;
hence
not createGraph ({1,2},{},S,S) is _trivial
; createGraph ({1,2},{},S,S) is simple
for e being object 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:76;
then A4:
createGraph ({1,2},{},S,S) is loopless
;
for e1, e2, v1, v2 being object st e1 Joins v1,v2, createGraph ({1,2},{},S,S) & e2 Joins v1,v2, createGraph ({1,2},{},S,S) holds
e1 = e2
by A2;
then
createGraph ({1,2},{},S,S) is non-multi
;
hence
createGraph ({1,2},{},S,S) is simple
by A4; verum