let G1 be _Graph; :: thesis: for G2 being Subgraph of G1 holds G2 .loops() c= G1 .loops()
let G2 be Subgraph of G1; :: thesis: G2 .loops() c= G1 .loops()

now :: thesis: for e being object st e in G2 .loops() holds
e in G1 .loops()

let e be object ; :: thesis: ( e in G2 .loops() implies e in G1 .loops() )
assume e in G2 .loops() ; :: thesis: e in G1 .loops()
then consider v being object such that
A1: e DJoins v,v,G2 by Th45;
( e is set & v is set ) by TARSKI:1;
hence e in G1 .loops() by A1, Th45, GLIB_000:72; :: thesis: verum

end;

hence G2 .loops() c= G1 .loops() by TARSKI:def 3; :: thesis: verum