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

now :: thesis: for e being object holds
( not e in the_Edges_of G2 or not (the_Source_of G2) . e = (the_Target_of G2) . e )

given e being object 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, Def32;
hence contradiction by A1, A2, Def18; :: thesis: verum

end;

hence G2 is loopless ; :: thesis: verum