let G be _Graph; :: thesis: for H being removeLoops of G holds
( the_Edges_of G = G .loops() iff H is edgeless )
let H be removeLoops of G; :: thesis: ( the_Edges_of G = G .loops() iff H is edgeless )
thus ( the_Edges_of G = G .loops() implies H is edgeless ) ; :: thesis: ( H is edgeless implies the_Edges_of G = G .loops() )
assume A1: H is edgeless ; :: thesis: the_Edges_of G = G .loops()
(the_Edges_of G) \ (G .loops()) = the_Edges_of H by GLIB_000:53
.= {} by A1 ;
then the_Edges_of G c= G .loops() by XBOOLE_1:37;
hence the_Edges_of G = G .loops() by XBOOLE_0:def 10; :: thesis: verum