let G1, G2 be _Graph; :: thesis: for F being PGraphMapping 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 PGraphMapping 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
for e being object holds
( not e in the_Edges_of G1 or not (the_Source_of G1) . e = (the_Target_of G1) . e )
proof
given e being object such that A3: e in the_Edges_of G1 and
A4: (the_Source_of G1) . e = (the_Target_of G1) . e ; :: thesis: contradiction
set v = (the_Source_of G1) . e;
A5: e Joins (the_Source_of G1) . e,(the_Source_of G1) . e,G1 by A3, A4, GLIB_000:def 13;
then (the_Source_of G1) . e in dom (F _V) by A1, GLIB_000:13;
then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Source_of G1) . e),G2 by A1, A3, A5, Th4;
hence contradiction by A2, GLIB_000:18; :: thesis: verum
end;
hence G1 is loopless by GLIB_000:def 18; :: thesis: verum
end;
thus ( G2 is edgeless implies G1 is edgeless ) by A1; :: thesis: verum