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

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

assume A2: G1 is loopless ; :: thesis: G2 is loopless
assume not G2 is loopless ; :: thesis: contradiction
then consider v being object such that
A3: ex e being object st e Joins v,v,G2 by GLIB_000:18;
consider e being object such that
A4: e Joins v,v,G2 by A3;
v in the_Vertices_of G2 by A4, GLIB_000:13;
then v in rng f by A1, FUNCT_2:def 3;
then consider v0 being object such that
A5: ( v0 in dom f & f . v0 = v ) by FUNCT_1:def 3;
consider e0 being object such that
A6: e0 Joins v0,v0,G1 by A4, A5, Th2;
thus contradiction by A2, A6, GLIB_000:18; :: thesis: verum

end;

hereby :: thesis: verum

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

end;