let G be _Graph; :: thesis: for H being removeLoops of G
for H9 being loopless Subgraph of G holds H9 is Subgraph of H
let H be removeLoops of G; :: thesis: for H9 being loopless Subgraph of G holds H9 is Subgraph of H
let H9 be loopless Subgraph of G; :: thesis: H9 is Subgraph of H
the_Vertices_of H = the_Vertices_of G by GLIB_000:53;
then A1: the_Vertices_of H9 c= the_Vertices_of H ;
A2: the_Edges_of H = (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
(the_Edges_of H9) /\ (G .loops()) = {}

proof

assume (the_Edges_of H9) /\ (G .loops()) <> {} ; :: thesis: contradiction
then consider x being object such that
A3: x in (the_Edges_of H9) /\ (G .loops()) by XBOOLE_0:def 1;
A4: ( x in the_Edges_of H9 & x in G .loops() ) by A3, XBOOLE_0:def 4;
then consider v being object such that
A5: x Joins v,v,G by GLIB_009:def 2;
( x is set & v is set ) by TARSKI:1;
then x Joins v,v,H9 by A4, A5, GLIB_000:73;
hence contradiction by GLIB_000:18; :: thesis: verum

end;

then the_Edges_of H9 misses G .loops() by XBOOLE_0:def 7;
hence H9 is Subgraph of H by A1, A2, XBOOLE_1:86, GLIB_000:44; :: thesis: verum