let G1, G2 be _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is total holds
( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )
let f be PVertexMapping of G1,G2; :: thesis: ( f is total implies ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) ) )
assume A1: f is total ; :: thesis: ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )

hereby :: thesis: ( G2 is edgeless implies G1 is edgeless )

assume A2: G2 is loopless ; :: thesis: G1 is loopless
assume not G1 is loopless ; :: thesis: contradiction
then consider v being object such that
A3: ex e being object st e Joins v,v,G1 by GLIB_000:18;
consider e being object such that
A4: e Joins v,v,G1 by A3;
v in the_Vertices_of G1 by A4, GLIB_000:13;
then v in dom f by A1, PARTFUN1:def 2;
then consider e9 being object such that
A5: e9 Joins f . v,f . v,G2 by A4, Th1;
thus contradiction by A2, A5, GLIB_000:18; :: thesis: verum

end;

hereby :: thesis: verum

assume A6: G2 is edgeless ; :: thesis: G1 is edgeless
assume not G1 is edgeless ; :: thesis: contradiction
then consider e being object such that
A7: e in the_Edges_of G1 by XBOOLE_0:def 1;
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
A8: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A7, GLIB_000:def 13;
then ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in the_Vertices_of G1 ) by GLIB_000:13;
then ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A1, FUNCT_2:def 1;
then consider e9 being object such that
A9: e9 Joins f . ((the_Source_of G1) . e),f . ((the_Target_of G1) . e),G2 by A8, Th1;
e9 in the_Edges_of G2 by A9, GLIB_000:def 13;
hence contradiction by A6; :: thesis: verum

end;