let G1, G2 be _Graph; 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; ( f is total implies ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) ) )
assume A1:
f is total
; ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )
hereby ( G2 is edgeless implies G1 is edgeless )
assume A2:
G2 is
loopless
;
G1 is loopless assume
not
G1 is
loopless
;
contradictionthen 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;
verum
end;