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) ; :: thesis: ( createGraph ({1,2},{},S,S) is _finite & not createGraph ({1,2},{},S,S) is _trivial & createGraph ({1,2},{},S,S) is simple )
thus createGraph ({1,2},{},S,S) is _finite ; :: 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 CARD_2:57;
hence not createGraph ({1,2},{},S,S) is _trivial ; :: thesis: createGraph ({1,2},{},S,S) is simple
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 ;
then createGraph ({1,2},{},S,S) is non-multi ;
hence createGraph ({1,2},{},S,S) is simple by A4; :: thesis: verum