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()

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()

hence
G2 .loops() c= G1 .loops()
by TARSKI:def 3; :: thesis: verume 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;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