let G2 be Subgraph of G; :: thesis: G2 is loopless

now

given e being set such that A1: e in the_Edges_of G2 and
A2: (the_Source_of G2) . e = (the_Target_of G2) . e ; :: thesis: contradiction
( (the_Source_of G2) . e = (the_Source_of G) . e & (the_Target_of G2) . e = (the_Target_of G) . e ) by A1, Def34;
hence contradiction by A1, A2, Def20; :: thesis: verum

end;

hence G2 is loopless by Def20; :: thesis: verum