the_Edges_of (createGraph e) = {e} by Th13;
hence not createGraph e is edgeless ; :: thesis: ( createGraph e is non-multi & createGraph e is connected & createGraph e is _finite )

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2, createGraph e & e2 Joins v1,v2, createGraph e holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2, createGraph e & e2 Joins v1,v2, createGraph e implies e1 = e2 )
assume ( e1 Joins v1,v2, createGraph e & e2 Joins v1,v2, createGraph e ) ; :: thesis: e1 = e2
then ( e1 in the_Edges_of (createGraph e) & e2 in the_Edges_of (createGraph e) ) by GLIB_000:def 13;
then ( e1 in {e} & e2 in {e} ) by Th13;
then ( e1 = e & e2 = e ) by TARSKI:def 1;
hence e1 = e2 ; :: thesis: verum

end;

hence createGraph e is non-multi by GLIB_000:def 20; :: thesis: ( createGraph e is connected & createGraph e is _finite )
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
for x, y being Vertex of (createGraph e) ex W being Walk of createGraph e st W is_Walk_from x,y

proof

let x, y be Vertex of (createGraph e); :: thesis: ex W being Walk of createGraph e st W is_Walk_from x,y

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: ex W being Walk of createGraph e st W is_Walk_from x,y

then (createGraph e) .walkOf x is_Walk_from x,y by GLIB_001:13;
hence ex W being Walk of createGraph e st W is_Walk_from x,y ; :: thesis: verum

end;

suppose A1: x <> y ; :: thesis: ex W being Walk of createGraph e st W is_Walk_from x,y

e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e by Th14;
then A2: ( e Joins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e & e Joins (the_Target_of G) . e,(the_Source_of G) . e, createGraph e ) by GLIB_000:16;
the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} by Th13;
then ( ( x = (the_Source_of G) . e or x = (the_Target_of G) . e ) & ( y = (the_Source_of G) . e or y = (the_Target_of G) . e ) ) by TARSKI:def 2;

per cases then ( ( x = (the_Source_of G) . e & y = (the_Target_of G) . e ) or ( x = (the_Target_of G) . e & y = (the_Source_of G) . e ) ) by A1;

suppose ( x = (the_Source_of G) . e & y = (the_Target_of G) . e ) ; :: thesis: ex W being Walk of createGraph e st W is_Walk_from x,y

then (createGraph e) .walkOf (((the_Source_of G) . e),e,((the_Target_of G) . e)) is_Walk_from x,y by A2, GLIB_001:15;
hence ex W being Walk of createGraph e st W is_Walk_from x,y ; :: thesis: verum

end;

suppose ( x = (the_Target_of G) . e & y = (the_Source_of G) . e ) ; :: thesis: ex W being Walk of createGraph e st W is_Walk_from x,y

then (createGraph e) .walkOf (((the_Target_of G) . e),e,((the_Source_of G) . e)) is_Walk_from x,y by A2, GLIB_001:15;
hence ex W being Walk of createGraph e st W is_Walk_from x,y ; :: thesis: verum

end;

end;

end;

end;

end;

hence createGraph e is connected by GLIB_002:def 1; :: thesis: createGraph e is _finite
( the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} & the_Edges_of (createGraph e) = {e} ) by Th13;
hence createGraph e is _finite by GLIB_000:def 17; :: thesis: verum