let G be simple _Graph; :: thesis: ex f being one-to-one Function st
( dom f = the_Edges_of G & rng f c= 2Set (the_Vertices_of G) & ( for e being object st e in dom f holds
f . e = {((the_Source_of G) . e),((the_Target_of G) . e)} ) )
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G and
A2: rng f c= (2Set (the_Vertices_of G)) \/ (singletons (the_Vertices_of G)) and
A3: for e being object st e in dom f holds
f . e = {((the_Source_of G) . e),((the_Target_of G) . e)} by Th4;
take f ; :: thesis: ( dom f = the_Edges_of G & rng f c= 2Set (the_Vertices_of G) & ( for e being object st e in dom f holds
f . e = {((the_Source_of G) . e),((the_Target_of G) . e)} ) )
(rng f) /\ (singletons (the_Vertices_of G)) = {}
proof
assume (rng f) /\ (singletons (the_Vertices_of G)) <> {} ; :: thesis: contradiction
then consider y being object such that
A4: y in (rng f) /\ (singletons (the_Vertices_of G)) by XBOOLE_0:def 1;
A5: ( y in rng f & y in singletons (the_Vertices_of G) ) by A4, XBOOLE_0:def 4;
then consider e being object such that
A6: ( e in dom f & f . e = y ) by FUNCT_1:def 3;
consider Y being Subset of (the_Vertices_of G) such that
A7: ( y = Y & Y is 1 -element ) by A5;
card Y = 1 by A7, CARD_1:def 7
.= card { the object } by CARD_1:30 ;
then consider v being object such that
A8: Y = {v} by CARD_1:29;
y = {((the_Source_of G) . e),((the_Target_of G) . e)} by A3, A6;
hence contradiction by A1, A6, A7, A8, ZFMISC_1:5, GLIB_000:def 18; :: thesis: verum
end;
hence ( dom f = the_Edges_of G & rng f c= 2Set (the_Vertices_of G) & ( for e being object st e in dom f holds
f . e = {((the_Source_of G) . e),((the_Target_of G) . e)} ) ) by A1, A2, A3, XBOOLE_1:73, XBOOLE_0:def 7; :: thesis: verum